1. Gul Agha and Karl Palmskog. A Survey of Statistical Model Checking. ACM Transactions on Modeling and Computer Simulation, 28(1):6:1-6:39, January 2018. ISSN: 1049-3301. Keyword(s): model checking. Abstract:

   Interactive, distributed, and embedded systems often behave stochastically, for example, when inputs, message delays, or failures conform to a probability distribution. However, reasoning analytically about the behavior of complex stochastic systems is generally infeasible. While simulations of systems are commonly used in engineering practice, they have not traditionally been used to reason about formal specifications. Statistical model checking (SMC) addresses this weakness by using a simulation-based approach to reason about precise properties specified in a stochastic temporal logic. A specification for a communication system may state that within some time bound, the probability that the number of messages in a queue will be greater than 5 must be less than 0.01. Using SMC, executions of a stochastic system are first sampled, after which statistical techniques are applied to determine whether such a property holds. While the output of sample-based methods are not always correct, statistical inference can quantify the confidence in the result produced. In effect, SMC provides a more widely applicable and scalable alternative to analysis of properties of stochastic systems using numerical and symbolic methods. SMC techniques have been successfully applied to analyze systems with large state spaces in areas such as computer networking, security, and systems biology. In this article, we survey SMC algorithms, techniques, and tools, while emphasizing current limitations and tradeoffs between precision and scalability.

   
   

   @article{aghaSurveyStatisticalModel2018,
   title = {A {{Survey}} of {{Statistical Model Checking}}},
   author = {Agha, Gul and Palmskog, Karl},
   year = {2018},
   month = jan,
   volume = {28},
   pages = {6:1--6:39},
   issn = {1049-3301},
   doi = {10.1145/3158668},
   abstract = {Interactive, distributed, and embedded systems often behave stochastically, for example, when inputs, message delays, or failures conform to a probability distribution. However, reasoning analytically about the behavior of complex stochastic systems is generally infeasible. While simulations of systems are commonly used in engineering practice, they have not traditionally been used to reason about formal specifications. Statistical model checking (SMC) addresses this weakness by using a simulation-based approach to reason about precise properties specified in a stochastic temporal logic. A specification for a communication system may state that within some time bound, the probability that the number of messages in a queue will be greater than 5 must be less than 0.01. Using SMC, executions of a stochastic system are first sampled, after which statistical techniques are applied to determine whether such a property holds. While the output of sample-based methods are not always correct, statistical inference can quantify the confidence in the result produced. In effect, SMC provides a more widely applicable and scalable alternative to analysis of properties of stochastic systems using numerical and symbolic methods. SMC techniques have been successfully applied to analyze systems with large state spaces in areas such as computer networking, security, and systems biology. In this article, we survey SMC algorithms, techniques, and tools, while emphasizing current limitations and tradeoffs between precision and scalability.},
   url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4360-Agha_Palmskog (2018) - A Survey of Statistical Model Checking.pdf},
   journal = {ACM Transactions on Modeling and Computer Simulation},
   keywords = {model checking},
   number = {1} 
   }
   




2. Laura Titolo, Marco A. Feliú, Mariano Moscato, and César A. Muñoz. An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs. In Isil Dillig and Jens Palsberg, editors, Verification, Model Checking, and Abstract Interpretation, volume 10747, pages 516-537. Springer International Publishing, Cham, 2018. ISBN: 978-3-319-73720-1 978-3-319-73721-8. Keyword(s): abstract interpretation. Abstract:

   This paper presents an abstract interpretation framework for the round-off error analysis of floating-point programs. This framework defines a parametric abstract analysis that computes, for each combination of ideal and floating-point execution path of the program, a sound over-approximation of the accumulated floating-point round-off error that may occur. In addition, a Boolean expression that characterizes the input values leading to the computed error approximation is also computed. An abstraction on the control flow of the program is proposed to mitigate the explosion of the number of elements generated by the analysis. Additionally, a widening operator is defined to ensure the convergence of recursive functions and loops. An instantiation of this framework is implemented in the prototype tool PRECiSA that generates formal proof certificates stating the correctness of the computed round-off errors.

   
   

   @incollection{titoloAbstractInterpretationFramework2018,
   title = {An {{Abstract Interpretation Framework}} for the {{Round}}-{{Off Error Analysis}} of {{Floating}}-{{Point Programs}}},
   booktitle = {Verification, {{Model Checking}}, and {{Abstract Interpretation}}},
   author = {Titolo, Laura and Feli{\'u}, Marco A. and Moscato, Mariano and Mu{\~n}oz, C{\'e}sar A.},
   editor = {Dillig, Isil and Palsberg, Jens},
   year = {2018},
   volume = {10747},
   pages = {516--537},
   publisher = {{Springer International Publishing}},
   address = {{Cham}},
   doi = {10.1007/978-3-319-73721-8_24},
   abstract = {This paper presents an abstract interpretation framework for the round-off error analysis of floating-point programs. This framework defines a parametric abstract analysis that computes, for each combination of ideal and floating-point execution path of the program, a sound over-approximation of the accumulated floating-point round-off error that may occur. In addition, a Boolean expression that characterizes the input values leading to the computed error approximation is also computed. An abstraction on the control flow of the program is proposed to mitigate the explosion of the number of elements generated by the analysis. Additionally, a widening operator is defined to ensure the convergence of recursive functions and loops. An instantiation of this framework is implemented in the prototype tool PRECiSA that generates formal proof certificates stating the correctness of the computed round-off errors.},
   url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4267-Titolo et al (2018) - An Abstract Interpretation Framework for the Round-Off Error Analysis of.pdf},
   isbn = {978-3-319-73720-1 978-3-319-73721-8},
   keywords = {abstract interpretation} 
   }
   

1. Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, and Deepak Garg. Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. In Amal Ahmed, editor, Programming Languages and Systems, Lecture Notes in Computer Science, Cham, pages 214-241, 2018. Springer International Publishing. ISBN: 978-3-319-89884-1. Keyword(s): calculus, probability. Abstract:

   We extend the simply-typed guarded extbackslash ( extbackslash lambda extbackslash )-calculus with discrete probabilities and endow it with a program logic for reasoning about relational properties of guarded probabilistic computations. This provides a framework for programming and reasoning about infinite stochastic processes like Markov chains. We demonstrate the logic sound by interpreting its judgements in the topos of trees and by using probabilistic couplings for the semantics of relational assertions over distributions on discrete types.The program logic is designed to support syntax-directed proofs in the style of relational refinement types, but retains the expressiveness of higher-order logic extended with discrete distributions, and the ability to reason relationally about expressions that have different types or syntactic structure. In addition, our proof system leverages a well-known theorem from the coupling literature to justify better proof rules for relational reasoning about probabilistic expressions. We illustrate these benefits with a broad range of examples that were beyond the scope of previous systems, including shift couplings and lump couplings between random walks.

   
   

   @inproceedings{aguirreRelationalReasoningMarkov2018,
   title = {Relational {{Reasoning}} for {{Markov Chains}} in a {{Probabilistic Guarded Lambda Calculus}}},
   booktitle = {Programming {{Languages}} and {{Systems}}},
   author = {Aguirre, Alejandro and Barthe, Gilles and Birkedal, Lars and Bizjak, Ale{\v s} and Gaboardi, Marco and Garg, Deepak},
   editor = {Ahmed, Amal},
   year = {2018},
   pages = {214--241},
   publisher = {{Springer International Publishing}},
   address = {{Cham}},
   doi = {10.1007/978-3-319-89884-1_8},
   abstract = {We extend the simply-typed guarded 	extbackslash (	extbackslash lambda 	extbackslash )-calculus with discrete probabilities and endow it with a program logic for reasoning about relational properties of guarded probabilistic computations. This provides a framework for programming and reasoning about infinite stochastic processes like Markov chains. We demonstrate the logic sound by interpreting its judgements in the topos of trees and by using probabilistic couplings for the semantics of relational assertions over distributions on discrete types.The program logic is designed to support syntax-directed proofs in the style of relational refinement types, but retains the expressiveness of higher-order logic extended with discrete distributions, and the ability to reason relationally about expressions that have different types or syntactic structure. In addition, our proof system leverages a well-known theorem from the coupling literature to justify better proof rules for relational reasoning about probabilistic expressions. We illustrate these benefits with a broad range of examples that were beyond the scope of previous systems, including shift couplings and lump couplings between random walks.},
   url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4409-Aguirre et al (2018) - Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda.pdf},
   isbn = {978-3-319-89884-1},
   keywords = {calculus,probability},
   series = {Lecture {{Notes}} in {{Computer Science}}} 
   }
   




2. Alexandra Bugariu, Valentin Wüstholz, Maria Christakis, and Peter Müller. Automatically Testing Implementations of Numerical Abstract Domains. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, New York, NY, USA, pages 768-778, 2018. ACM. ISBN: 978-1-4503-5937-5. Keyword(s): abstract interpretation. Abstract:

   Static program analyses are routinely applied as the basis of code optimizations and to detect safety and security issues in software systems. For their results to be reliable, static analyses should be sound (i.e., should not produce false negatives) and precise (i.e., should report a low number of false positives). Even though it is possible to prove properties of the design of a static analysis, ensuring soundness and precision for its implementation is challenging. Complex algorithms and sophisticated optimizations make static analyzers difficult to implement and test. In this paper, we present an automatic technique to test, among other properties, the soundness and precision of abstract domains, the core of all static analyzers based on abstract interpretation. In order to cover a wide range of test data and input states, we construct inputs by applying sequences of abstract-domain operations to representative domain elements, and vary the operations through gray-box fuzzing. We use mathematical properties of abstract domains as test oracles. Our experimental evaluation demonstrates the effectiveness of our approach. We detected several previously unknown soundness and precision errors in widely-used abstract domains. Our experiments also show that our approach is more effective than dynamic symbolic execution and than fuzzing the test inputs directly.

   
   

   @inproceedings{bugariuAutomaticallyTestingImplementations2018,
   title = {Automatically {{Testing Implementations}} of {{Numerical Abstract Domains}}},
   booktitle = {Proceedings of the 33rd {{ACM}}/{{IEEE International Conference}} on {{Automated Software Engineering}}},
   author = {Bugariu, Alexandra and W{\"u}stholz, Valentin and Christakis, Maria and M{\"u}ller, Peter},
   year = {2018},
   pages = {768--778},
   publisher = {{ACM}},
   address = {{New York, NY, USA}},
   doi = {10.1145/3238147.3240464},
   abstract = {Static program analyses are routinely applied as the basis of code optimizations and to detect safety and security issues in software systems. For their results to be reliable, static analyses should be sound (i.e., should not produce false negatives) and precise (i.e., should report a low number of false positives). Even though it is possible to prove properties of the design of a static analysis, ensuring soundness and precision for its implementation is challenging. Complex algorithms and sophisticated optimizations make static analyzers difficult to implement and test. In this paper, we present an automatic technique to test, among other properties, the soundness and precision of abstract domains, the core of all static analyzers based on abstract interpretation. In order to cover a wide range of test data and input states, we construct inputs by applying sequences of abstract-domain operations to representative domain elements, and vary the operations through gray-box fuzzing. We use mathematical properties of abstract domains as test oracles. Our experimental evaluation demonstrates the effectiveness of our approach. We detected several previously unknown soundness and precision errors in widely-used abstract domains. Our experiments also show that our approach is more effective than dynamic symbolic execution and than fuzzing the test inputs directly.},
   url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/3994-Bugariu et al (2018) - Automatically Testing Implementations of Numerical Abstract Domains.pdf},
   isbn = {978-1-4503-5937-5},
   keywords = {abstract interpretation},
   series = {{{ASE}} 2018} 
   }
   




3. Matthew Mirman, Timon Gehr, and Martin Vechev. Differentiable Abstract Interpretation for Provably Robust Neural Networks. In International Conference on Machine Learning, pages 3578-3586, July 2018. Keyword(s): abstract interpretation. Abstract:

   We introduce a scalable method for training robust neural networks based on abstract interpretation. We present several abstract transformers which balance efficiency with precision and show these ...

   
   

   @inproceedings{mirmanDifferentiableAbstractInterpretation2018,
   title = {Differentiable {{Abstract Interpretation}} for {{Provably Robust Neural Networks}}},
   booktitle = {International {{Conference}} on {{Machine Learning}}},
   author = {Mirman, Matthew and Gehr, Timon and Vechev, Martin},
   year = {2018},
   month = jul,
   pages = {3578--3586},
   abstract = {We introduce a scalable method for training robust neural networks based on abstract interpretation. We present several abstract transformers which balance efficiency with precision and show these ...},
   url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4060-Mirman et al (2018) - Differentiable Abstract Interpretation for Provably Robust Neural Networks.pdf},
   keywords = {abstract interpretation} 
   }
   




4. Anthony Narkawicz, Cesar Munoz, and Aaron Dutle. The MINERVA Software Development Process. In Automated Formal Methods, volume 5 of Kalpa Publications in Computing, pages 93-108, 2018. ISSN: 2515-1762. Keyword(s): avionics, verification.
   

   @inproceedings{narkawiczMINERVASoftwareDevelopment2018,
   title = {The {{MINERVA Software Development Process}}},
   booktitle = {Automated {{Formal Methods}}},
   author = {Narkawicz, Anthony and Munoz, Cesar and Dutle, Aaron},
   year = {2018},
   volume = {5},
   pages = {93--108},
   issn = {2515-1762},
   doi = {10.29007/5jlw},
   url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4269-Narkawicz et al (2018) - The MINERVA Software Development Process.pdf},
   keywords = {avionics,verification},
   series = {Kalpa {{Publications}} in {{Computing}}} 
   }
   

1. Raphaël Monat. Static Analysis by Abstract Interpretation Collecting Types of Python Programs. Intership Report, LIP6 - Laboratoire d'Informatique de Paris 6, September 2018. Keyword(s): abstract interpretation. Abstract:

   Software bugs are costly: they can have disastrous consequences on critical systems, but also on more common applications such as Web servers. It is thus interesting to possess tools helping developers detect those bugs before they ship software into production. The most common approach to avoid those errors is to use testing, which is inefficient: tests are usually written by hand, taking time, and they cover a few executions of a program, but not all of them. The approach I undertook during this internship is to design a static analyzer by abstract interpretation for Python. Static analyzers are programs that automatically analyze an input program and report errors this input program may contain (given a certain class of errors the static analyzer may detect). In particular, if a static analyzer is sound and reports no error on a given input, we know that this program does not contain any error from the class the static analyzer is able to discover. Abstract interpretation is a theory formalizing links between a precise but costly semantics with some computable, approximated counterpart, thus guiding the design and implementation of sound static analyzers. State of the art static analyzers include Julia (analyzing Java), Astr\'ee and Sparrow (for C software). Those are only analyzing statically typed languages. There are no mature static analyzers available for dynamic languages such as JavaScript and Python, although a few static analyses have already been developed and implemented. During this internship, I developed a static analysis of Python programs collecting the types of each variable, and possible type error exceptions. Python is a popular programming language, especially used in teaching and in the scientific community, well-known for its powerful syntax. Major software projects written in Python include the Django web framework and the SageMath computer algebra system. Python is an object-oriented dynamic language, where every value is an object. Python's dynamism means that undeclared variables, type incompatibilities, extbackslash dots extbackslash, are exceptions detected at runtime.

   
   

   @techreport{monatStaticAnalysisAbstract2018,
   title = {Static {{Analysis}} by {{Abstract Interpretation Collecting Types}} of {{Python Programs}}},
   author = {Monat, Rapha{\"e}l},
   year = {2018},
   month = sep,
   institution = {{LIP6 - Laboratoire d'Informatique de Paris 6}},
   abstract = {Software bugs are costly: they can have disastrous consequences on critical systems, but also on more common applications such as Web servers. It is thus interesting to possess tools helping developers detect those bugs before they ship software into production. The most common approach to avoid those errors is to use testing, which is inefficient: tests are usually written by hand, taking time, and they cover a few executions of a program, but not all of them. The approach I undertook during this internship is to design a static analyzer by abstract interpretation for Python. Static analyzers are programs that automatically analyze an input program and report errors this input program may contain (given a certain class of errors the static analyzer may detect). In particular, if a static analyzer is sound and reports no error on a given input, we know that this program does not contain any error from the class the static analyzer is able to discover. Abstract interpretation is a theory formalizing links between a precise but costly semantics with some computable, approximated counterpart, thus guiding the design and implementation of sound static analyzers. State of the art static analyzers include Julia (analyzing Java), Astr\'ee and Sparrow (for C software). Those are only analyzing statically typed languages. There are no mature static analyzers available for dynamic languages such as JavaScript and Python, although a few static analyses have already been developed and implemented. During this internship, I developed a static analysis of Python programs collecting the types of each variable, and possible type error exceptions. Python is a popular programming language, especially used in teaching and in the scientific community, well-known for its powerful syntax. Major software projects written in Python include the Django web framework and the SageMath computer algebra system. Python is an object-oriented dynamic language, where every value is an object. Python's dynamism means that undeclared variables, type incompatibilities, 	extbackslash dots	extbackslash, are exceptions detected at runtime.},
   url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4102-Monat (2018) - Static Analysis by Abstract Interpretation Collecting Types of Python Programs.pdf},
   type = {Intership Report},
   keywords = {abstract interpretation} 
   }
   

1. Reynald Affeldt, Cyril Cohen, Assia Mahboubi, Damien Rouhling, and Pierre-Yves Strub. Classical Analysis with Coq, 2018. Keyword(s): Coq.
   

   @misc{affeldtClassicalAnalysisCoq2018,
   title = {Classical Analysis with {{Coq}}},
   author = {Affeldt, Reynald and Cohen, Cyril and Mahboubi, Assia and Rouhling, Damien and Strub, Pierre-Yves},
   year = {2018},
   url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4338-Affeldt et al (2018) - Classical analysis with Coq.pdf},
   keywords = {Coq},
   
   }
   

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Les documents contenus dans ces répertoires sont rendus disponibles par les auteurs qui y ont contribué en vue d'assurer la diffusion à temps de travaux savants et techniques sur une base non-commerciale. Les droits de copie et autres droits sont gardés par les auteurs et par les détenteurs du copyright, en dépit du fait qu'ils présentent ici leurs travaux sous forme électronique. Les personnes copiant ces informations doivent adhérer aux termes et contraintes couverts par le copyright de chaque auteur. Ces travaux ne peuvent pas être rendus disponibles ailleurs sans la permission explicite du détenteur du copyright.

This document was translated from BibT_EX by bibtex2html