1. Reynald Affeldt, Jacques Garrigue, David Nowak, and Takafumi Saikawa. A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism. arXiv:2003.09993 [cs], March 2020. Keyword(s): probability. Abstract:

   REYNALD AFFELDT, National Institute of Advanced Industrial Science and Technology, Japan JACQUES GARRIGUE, Nagoya University, Japan DAVID NOWAK, CNRS \& Lille University, France TAKAFUMI SAIKAWA, Nagoya University, Japan The algebraic properties of the combination of probabilistic choice and nondeterministic choice have long been a research topic in program semantics. This paper explains a formalization (the first one to the best of our knowledge) in the Coq proof assistant of a monad equipped with both choices: the geometrically convex monad. This formalization has an immediate application: it provides a model for a monad that implements a non-trivial interface which allows for proofs by equational reasoning using probabilistic and nondeterministic effects. We explain the technical choices we made to go from the literature to a complete Coq formalization, from which we identify reusable theories about mathematical structures such as convex spaces and concrete categories.

   [bibtex-key = affeldtTrustfulMonadAxiomatic2020] [bibtex-entry]



2. Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa. A Library for Formalization of Linear Error-Correcting Codes. Journal of Automated Reasoning, January 2020. ISSN: 1573-0670. Keyword(s): Coq, probability. Abstract:

   Error-correcting codes add redundancy to transmitted data to ensure reliable communication over noisy channels. Since they form the foundations of digital communication, their correctness is a matter of concern. To enable trustful verification of linear error-correcting codes, we have been carrying out a systematic formalization in the Coq proof-assistant. This formalization includes the material that one can expect of a university class on the topic: the formalization of well-known codes (Hamming, Reed- Solomon, Bose- Chaudhuri- Hocquenghem) and also a glimpse at modern coding theory. We demonstrate the usefulness of our formalization by extracting a verified decoder for low-density parity-check codes based on the sum-product algorithm. To achieve this formalization, we needed to develop a number of libraries on top of Coq's Mathematical Components. Special care was taken to make them as reusable as possible so as to help implementers and researchers dealing with error-correcting codes in the future.

   [bibtex-key = affeldtLibraryFormalizationLinear2020] [bibtex-entry]



3. Davide Ancona, Pietro Barbieri, Francesco Dagnino, and Elena Zucca. Sound Regular Corecursion in coFJ. arXiv:2005.14085 [cs], May 2020. Keyword(s): Java, streams. Abstract:

   The aim of the paper is to provide solid foundations for a programming paradigm natively supporting the creation and manipulation of cyclic data structures. To this end, we describe coFJ, a Java-like calculus where objects can be infinite and methods are equipped with a codefinition (an alternative body). We provide an abstract semantics of the calculus based on the framework of inference systems with corules. In coFJ with this semantics, FJ recursive methods on finite objects can be extended to infinite objects as well, and behave as desired by the programmer, by specifying a codefinition. We also describe an operational semantics which can be directly implemented in a programming language, and prove the soundness of such semantics with respect to the abstract one.

   [bibtex-key = anconaSoundRegularCorecursion2020] [bibtex-entry]



4. Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. Abstract Interpretation of Distributed Network Control Planes. Proceedings of the ACM on Programming Languages, 4(POPL):1-27, January 2020. ISSN: 2475-1421, 2475-1421. Keyword(s): abstract interpretation. [bibtex-key = beckettAbstractInterpretationDistributed2020] [bibtex-entry]



5. Gianluca Curzi and Luca Roversi. Probabilistic Soft Type Assignment. arXiv:2007.01733 [cs], July 2020. Keyword(s): calculus, probability. Abstract:

   We model randomized complexity classes in the style of Implicit Computational Complexity. We introduce PSTA, a probabilistic version of STA, the type-theoretical counterpart of Soft Linear Logic. PSTA is a type assignment for an extension of Simpson's Linear Lambda Calculus and its surface reduction, where Linear additives express random choice. Linear additives are weaker than the usual ones; they allow for duplications harmlessly affecting the computational cost of normalization. PSTA is sound and complete w.r.t. probabilistic polynomial time functions and characterizes the probabilistic complexity classes PP and BPP, the latter slightly less implicitly than PP.

   [bibtex-key = curziProbabilisticSoftType2020] [bibtex-entry]

1. B. Lacerda, F. Faruq, D. Parker, and N. Hawes. Probabilistic Planning with Formal Performance Guarantees for Mobile Service Robots. International Journal of Robotics Research, 38(19):1098-1123, 2019. Keyword(s): model checking, probability. [bibtex-key = lacerdaProbabilisticPlanningFormal2019] [bibtex-entry]



2. Changliu Liu, Tomer Arnon, Christopher Lazarus, Clark Barrett, and Mykel J. Kochenderfer. Algorithms for Verifying Deep Neural Networks. arXiv:1903.06758 [cs, stat], March 2019. Keyword(s): model checking. Abstract:

   Deep neural networks are widely used for nonlinear function approximation with applications ranging from computer vision to control. Although these networks involve the composition of simple arithmetic operations, it can be very challenging to verify whether a particular network satisfies certain input-output properties. This article surveys methods that have emerged recently for soundly verifying such properties. These methods borrow insights from reachability analysis, optimization, and search. We discuss fundamental differences and connections between existing algorithms. In addition, we provide pedagogical implementations of existing methods and compare them on a set of benchmark problems.

   [bibtex-key = liuAlgorithmsVerifyingDeep2019] [bibtex-entry]



3. C. Faggian and S. R. d Rocca. Lambda Calculus and Probabilistic Computation. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13, June 2019. Keyword(s): calculus, probability. Abstract:

   We introduce two extensions of the {$\lambda$} -calculus with a probabilistic choice operator, {$\Lambda\oplus$}cbv and {$\Lambda\oplus$}cbn, modeling respectively call-by-value and call-by-name probabilistic computation. We prove that both enjoys confluence and standardization, in an extended way: we revisit these two fundamental notions to take into account the asymptotic behaviour of terms. The common root of the two calculi is a further calculus based on Linear Logic, {$\Lambda\oplus$}!, which allows us to develop a unified, modular approach.

   [bibtex-key = faggianLambdaCalculusProbabilistic2019] [bibtex-entry]



4. M. Kwiatkowska, G. Norman, and D. Parker. Verification and Control of Turn-Based Probabilistic Real-Time Games. In M. Alvim, K. Chatzikokolakis, C. Olarte, and F. Valencia, editors, The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy (Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday), volume 11760 of LNCS, pages 379-396, 2019. Springer. Keyword(s): model checking, probability. [bibtex-key = kwiatkowskaVerificationControlTurnBased2019] [bibtex-entry]



5. Wenbo Zhang, Huan Long, and Xian Xu. Uniform Random Process Model Revisited. In Anthony Widjaja Lin, editor, Programming Languages and Systems, Lecture Notes in Computer Science, Cham, pages 388-404, 2019. Springer International Publishing. ISBN: 978-3-030-34175-6. Keyword(s): pi calculus, calculus, probability. Abstract:

   Recently, a proper bisimulation equivalence relation for random process model has been defined in a model independent approach. Model independence clarifies the difference between nondeterministic and probabilistic actions in concurrency and makes the new equivalence relation to be congruent. In this paper, we focus on the finite state randomized CCS model and deepen the previous work in two aspects. First, we show that the equivalence relation can be decided in polynomial time. Second, we give a sound and complete axiomatization system for this model. The algorithm and axiomatization system also have the merit of model independency as they can be easily generalized to the randomized extension of any finite state concurrent model.

   [bibtex-key = zhangUniformRandomProcess2019] [bibtex-entry]



6. Donnacha Oisìn Kidney. Probability Monads in Cubical Agda. https://doisinkidney.com/posts/2019-04-17-cubical-probability.html, April 2019. Keyword(s): probability. [bibtex-key = kidneyProbabilityMonadsCubical2019] [bibtex-entry]



7. Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa. Reasoning with Conditional Probabilities and Joint Distributions in Coq. , March 2019. Keyword(s): Coq, probability. Abstract:

   Probabilities occur in many applications of computer science, such as communication theory and artificial intelligence. These are critical applications that require some form of verification to guarantee the quality of their implementations. Unfortunately, probabilities are also the typical example of a mathematical theory whose abuses of notations make pencil-and-paper proofs difficult to formalize. In this paper, we experiment a new formalization of conditional probabilities that we validate with two applications. First, we formalize the foundational definitions and theorems of information theory, extending previous work with new lemmas. Second, we formalize the notion of conditional independence and its properties, paving the road for a formalization of graphical probabilistic models.

   [bibtex-key = affeldtReasoningConditionalProbabilities2019] [bibtex-entry]

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.

   [bibtex-key = aghaSurveyStatisticalModel2018] [bibtex-entry]



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.

   [bibtex-key = titoloAbstractInterpretationFramework2018] [bibtex-entry]



3. 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.

   [bibtex-key = aguirreRelationalReasoningMarkov2018] [bibtex-entry]



4. 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.

   [bibtex-key = bugariuAutomaticallyTestingImplementations2018] [bibtex-entry]



5. 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 ...

   [bibtex-key = mirmanDifferentiableAbstractInterpretation2018] [bibtex-entry]



6. 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. [bibtex-key = narkawiczMINERVASoftwareDevelopment2018] [bibtex-entry]



7. 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.

   [bibtex-key = monatStaticAnalysisAbstract2018] [bibtex-entry]



8. Reynald Affeldt, Cyril Cohen, Assia Mahboubi, Damien Rouhling, and Pierre-Yves Strub. Classical Analysis with Coq, 2018. Keyword(s): Coq. [bibtex-key = affeldtClassicalAnalysisCoq2018] [bibtex-entry]

1. Daniel Ricketts. Verification of Sampled-Data Systems Using Coq. PhD Thesis, University of California, San Diego, 2017. Keyword(s): Coq, verification. [bibtex-key = rickettsVerificationSampleddataSystems2017] [bibtex-entry]



2. Jeremy Avigad, Johannes Hölzl, and Luke Serafin. A Formally Verified Proof of the Central Limit Theorem. Journal of Automated Reasoning, 59(4):389-423, December 2017. ISSN: 1573-0670. Keyword(s): HOL, Isabelle, probability. Abstract:

   We describe a proof of the Central Limit Theorem that has been formally verified in the Isabelle proof assistant. Our formalization builds upon and extends Isabelle's libraries for analysis and measure-theoretic probability. The proof of the theorem uses characteristic functions, which are a kind of Fourier transform, to demonstrate that, under suitable hypotheses, sums of random variables converge weakly to the standard normal distribution. We also discuss the libraries and infrastructure that supported the formalization, and reflect on some of the lessons we have learned from the effort.

   [bibtex-key = avigadFormallyVerifiedProof2017] [bibtex-entry]



3. Ranald Clouston, Ales Bizjak, Hans Bugge Grathwohl, and Lars Birkedal. The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. Logical Methods in Computer Science, 12(3):7, April 2017. ISSN: 18605974. Keyword(s): calculus, streams. Abstract:

   We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures the productivity of well-typed programs. Guarded recursive types may be transformed into coinductive types by a type-former inspired by modal logic and Atkey-McBride clock quantification, allowing the typing of acausal functions. We give a call-by-name operational semantics for the calculus, and define adequate denotational semantics in the topos of trees. The adequacy proof entails that the evaluation of a program always terminates. We introduce a program logic with L extbackslash ob induction for reasoning about the contextual equivalence of programs. We demonstrate the expressiveness of the calculus by showing the definability of solutions to Rutten's behavioural differential equations.

   [bibtex-key = cloustonGuardedLambdaCalculusProgramming2017] [bibtex-entry]



4. M. Kwiatkowska, G. Norman, and D. Parker. Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic Timed Automata. In Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, volume 10460 of LNCS, pages 289-309, 2017. Springer. Keyword(s): model checking, probability. [bibtex-key = kwiatkowskaSymbolicVerificationStrategy2017] [bibtex-entry]



5. Gagandeep Singh, Markus Püschel, and Martin Vechev. Fast Polyhedra Abstract Domain. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, New York, NY, USA, pages 46-59, 2017. ACM. ISBN: 978-1-4503-4660-3. Keyword(s): abstract interpretation. Abstract:

   Numerical abstract domains are an important ingredient of modern static analyzers used for verifying critical program properties (e.g., absence of buffer overflow or memory safety). Among the many numerical domains introduced over the years, Polyhedra is the most expressive one, but also the most expensive: it has worst-case exponential space and time complexity. As a consequence, static analysis with the Polyhedra domain is thought to be impractical when applied to large scale, real world programs. In this paper, we present a new approach and a complete implementation for speeding up Polyhedra domain analysis. Our approach does not lose precision, and for many practical cases, is orders of magnitude faster than state-of-the-art solutions. The key insight underlying our work is that polyhedra arising during analysis can usually be kept decomposed, thus considerably reducing the overall complexity. We first present the theory underlying our approach, which identifies the interaction between partitions of variables and domain operators. Based on the theory we develop new algorithms for these operators that work with decomposed polyhedra. We implemented these algorithms using the same interface as existing libraries, thus enabling static analyzers to use our implementation with little effort. In our evaluation, we analyze large benchmarks from the popular software verification competition, including Linux device drivers with over 50K lines of code. Our experimental results demonstrate massive gains in both space and time: we show end-to-end speedups of two to five orders of magnitude compared to state-of-the-art Polyhedra implementations as well as significant memory gains, on all larger benchmarks. In fact, in many cases our analysis terminates in seconds where prior code runs out of memory or times out after 4 hours. We believe this work is an important step in making the Polyhedra abstract domain both feasible and practically usable for handling large, real-world programs.

   [bibtex-key = singhFastPolyhedraAbstract2017] [bibtex-entry]

1. Matthew Chan, Daniel Ricketts, Sorin Lerner, and Gregory Malecha. Formal Verification of Stability Properties of Cyber-Physical Systems. pp 2, 2016. Keyword(s): Coq, verification. [bibtex-key = chanFormalVerificationStability2016] [bibtex-entry]



2. Robert Kelly, Barak A. Pearlmutter, and Jeffrey Mark Siskind. Evolving the Incremental Lambda Calculus into a Model of Forward Automatic Differentiation (AD). arXiv:1611.03429 [cs], November 2016. Keyword(s): calculus. Abstract:

   Formal transformations somehow resembling the usual derivative are surprisingly common in computer science, with two notable examples being derivatives of regular expressions and derivatives of types. A newcomer to this list is the incremental \$ extbackslash lambda\$-calculus, or ILC, a "theory of changes" that deploys a formal apparatus allowing the automatic generation of efficient update functions which perform incremental computation. The ILC is not only defined, but given a formal machine-understandable definition---accompanied by mechanically verifiable proofs of various properties, including in particular correctness of various sorts. Here, we show how the ILC can be mutated into propagating tangents, thus serving as a model of Forward Accumulation Mode Automatic Differentiation. This mutation is done in several steps. These steps can also be applied to the proofs, resulting in machine-checked proofs of the correctness of this model of forward AD.

   [bibtex-key = kellyEvolvingIncrementalLambda2016] [bibtex-entry]



3. Stefan Mitsch and André Platzer. ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models. Formal Methods in System Design, 49(1):33-74, October 2016. ISSN: 1572-8102. Keyword(s): verification. Abstract:

   Formal verification and validation play a crucial role in making cyber-physical systems (CPS) safe. Formal methods make strong guarantees about the system behavior if accurate models of the system can be obtained, including models of the controller and of the physical dynamics. In CPS, models are essential; but any model we could possibly build necessarily deviates from the real world. If the real system fits to the model, its behavior is guaranteed to satisfy the correctness properties verified with respect to the model. Otherwise, all bets are off. This article introduces ModelPlex, a method ensuring that verification results about models apply to CPS implementations. ModelPlex provides correctness guarantees for CPS executions at runtime: it combines offline verification of CPS models with runtime validation of system executions for compliance with the model. ModelPlex ensures in a provably correct way that the verification results obtained for the model apply to the actual system runs by monitoring the behavior of the world for compliance with the model. If, at some point, the observed behavior no longer complies with the model so that offline verification results no longer apply, ModelPlex initiates provably safe fallback actions, assuming the system dynamics deviation is bounded. This article, furthermore, develops a systematic technique to synthesize provably correct monitors automatically from CPS proofs in differential dynamic logic by a correct-by-construction approach, leading to verifiably correct runtime model validation. Overall, ModelPlex generates provably correct monitor conditions that, if checked to hold at runtime, are provably guaranteed to imply that the offline safety verification results about the CPS model apply to the present run of the actual CPS implementation.

   [bibtex-key = mitschModelPlexVerifiedRuntime2016] [bibtex-entry]



4. Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. A Lambda-Calculus Foundation for Universal Probabilistic Programming. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming - ICFP 2016, Nara, Japan, pages 33-46, 2016. ACM Press. ISBN: 978-1-4503-4219-3. Keyword(s): calculus, probability. Abstract:

   We develop the operational semantics of an untyped probabilistic {$\lambda$}-calculus with continuous distributions, and both hard and soft constraints, as a foundation for universal probabilistic programming languages such as CHURCH, ANGLICAN, and VENTURE. Our first contribution is to adapt the classic operational semantics of {$\lambda$}-calculus to a continuous setting via creating a measure space on terms and defining step-indexed approximations. We prove equivalence of big-step and small-step formulations of this distribution-based semantics. To move closer to inference techniques, we also define the sampling-based semantics of a term as a function from a trace of random samples to a value. We show that the distribution induced by integration over the space of traces equals the distribution-based semantics. Our second contribution is to formalize the implementation technique of trace Markov chain Monte Carlo (MCMC) for our calculus and to show its correctness. A key step is defining sufficient conditions for the distribution induced by trace MCMC to converge to the distribution-based semantics. To the best of our knowledge, this is the first rigorous correctness proof for trace MCMC for a higher-order functional language, or for a language with soft constraints.

   [bibtex-key = borgstromLambdacalculusFoundationUniversal2016] [bibtex-entry]



5. Maria Consiglio, Cesar Munoz, George Hagen, Anthony Narkawicz, and Swee Balachandran. ICAROUS: Integrated Configurable Algorithms for Reliable Operations of Unmanned Systems. In 2016 IEEE/AIAA 35th Digital Avionics Systems Conference (DASC), Sacramento, CA, USA, pages 1-5, September 2016. IEEE. ISBN: 978-1-5090-2523-7. Keyword(s): avionics, verification. Abstract:

   NASA's Unmanned Aerial System (UAS) Traffic Management (UTM) project aims at enabling near-term, safe operations of small UAS vehicles in uncontrolled airspace, i.e., Class G airspace. A far-term goal of UTM research and development is to accommodate the expected rise in small UAS traffic density throughout the National Airspace System (NAS) at low altitudes for beyond visual line-of-sight operations. This paper describes a new capability referred to as ICAROUS (Integrated Configurable Algorithms for Reliable Operations of Unmanned Systems), which is being developed under the UTM project. ICAROUS is a software architecture comprised of highly assured algorithms for building safety-centric, autonomous, unmanned aircraft applications. Central to the development of the ICAROUS algorithms is the use of well-established formal methods to guarantee higher levels of safety assurance by monitoring and bounding the behavior of autonomous systems. The core autonomy-enabling capabilities in ICAROUS include constraint conformance monitoring and contingency control functions. ICAROUS also provides a highly configurable user interface that enables the modular integration of mission-specific software components.

   [bibtex-key = consiglioICAROUSIntegratedConfigurable2016] [bibtex-entry]



6. Gregory Malecha, Daniel Ricketts, Mario M. Alvarez, and Sorin Lerner. Towards Foundational Verification of Cyber-Physical Systems. In 2016 Science of Security for Cyber-Physical Systems Workshop (SOSCYPS), Vienna, Austria, pages 1-5, April 2016. IEEE. ISBN: 978-1-5090-4304-0. Keyword(s): verification. Abstract:

   The safety-critical aspects of cyber-physical systems motivate the need for rigorous analysis of these systems. In the literature this work is often done using idealized models of systems where the analysis can be carried out using highlevel reasoning techniques such as Lyapunov functions and model checking. In this paper we present VERIDRONE, a foundational framework for reasoning about cyber-physical systems at all levels from high-level models to C code that implements the system. VERIDRONE is a library within the Coq proof assistant enabling us to build on its foundational implementation, its interactive development environments, and its wealth of libraries capturing interesting theories ranging from real numbers and differential equations to verified compilers and floating point numbers. These features make proof assistants in general, and Coq in particular, a powerful platform for unifying foundational results about safetycritical systems and ensuring interesting properties at all levels of the stack.

   [bibtex-key = malechaFoundationalVerificationCyberphysical2016] [bibtex-entry]



7. Muhammad Qasim, Osman Hasan, Maissa Elleuch, and Sofiène Tahar. Formalization of Normal Random Variables in HOL. In Michael Kohlhase, Moa Johansson, Bruce Miller, Leonardo de Moura, and Frank Tompa, editors, Intelligent Computer Mathematics, Lecture Notes in Computer Science, Cham, pages 44-59, 2016. Springer International Publishing. ISBN: 978-3-319-42547-4. Keyword(s): HOL, probability. Abstract:

   Many components of engineering systems exhibit random and uncertain behaviors that are normally distributed. In order to conduct the analysis of such systems within the trusted kernel of a higher-order-logic theorem prover, in this paper, we provide a higher-order-logic formalization of Lebesgue measure and Normal random variables along with the proof of their classical properties. To illustrate the usefulness of our formalization, we present a formal analysis of the probabilistic clock synchronization in wireless sensor networks.

   [bibtex-key = qasimFormalizationNormalRandom2016] [bibtex-entry]



8. Daniel Ricketts, Gregory Malecha, and Sorin Lerner. Modular Deductive Verification of Sampled-Data Systems. In Proceedings of the 13th International Conference on Embedded Software - EMSOFT '16, Pittsburgh, Pennsylvania, pages 1-10, 2016. ACM Press. ISBN: 978-1-4503-4485-2. Keyword(s): verification. Abstract:

   Unsafe behavior of cyber-physical systems can have disastrous consequences, motivating the need for formal verification of these kinds of systems. Deductive verification in a proof assistant such as Coq is a promising technique for this verification because it (1) justifies all verification from first principles, (2) is not limited to classes of systems for which full automation is possible, and (3) provides a platform for proving powerful, higher-order modularity theorems that are crucial for scaling verification to complex systems. In this paper, we demonstrate the practicality, utility, and scalability of this approach by developing in Coq sound and powerful rules for modular construction and verification of sampleddata cyber-physical systems. We evaluate these rules by using them to verify a number of non-trivial controllers enforcing safety properties of a quadcopter, e.g. a geo-fence. We show that our controllers are realistic by running them on a real, flying quadcopter.

   [bibtex-key = rickettsModularDeductiveVerification2016] [bibtex-entry]

1. Caterina Urban. Static Analysis by Abstract Interpretation of Functional Temporal Properties of Programs. PhD thesis, Ecole normale supérieure - ENS PARIS, July 2015. Keyword(s): abstract interpretation. Abstract:

   The overall aim of this thesis is the development of mathematically sound and practically efficient methods for automatically proving the correctness of computer software. More specifically, this thesis is grounded in the theory of abstract interpretation, a powerful mathematical framework for approximating the behavior of programs. In particular, this thesis focuses on provingprogram liveness properties, which represent requirements that must be eventually or repeatedly realized during program execution. Program termination is the most prominent liveness property. This thesis designs new program approximations, in order to automatically infer sufficient preconditions for program termination and synthesize so called piecewisedefined ranking functions, which provide upper bounds on the waiting time before termination. The approximations are parametric in the choice between the expressivity and the cost of the underlying approximations, which maintain information about the set of possible values of the program variables along with the possible numerical relationships between them. This thesis also contributes an abstract interpretation framework for proving liveness properties, which comes as a generalization of the framework proposedfor termination. In particular, the framework is dedicated to liveness properties expressed in temporal logic, which are used to ensure that some desirable event happens once or infinitely many times during program execution. As for program termination, piecewise-defined ranking functions are used to infer sufficient preconditions for these properties, and to provide upper boundson the waiting time before a desirable event. The results presented in this thesis have been implemented into a prototype analyzer. Experimental results show that it performs well on a wide variety of benchmarks, it is competitive with the state of the art, and is able to analyze programs that are out of the reach of existing methods.

   [bibtex-key = urbanStaticAnalysisAbstract2015] [bibtex-entry]



2. Stefan Milius and Thorsten Wissmann. Finitary Corecursion for the Infinitary Lambda Calculus. arXiv:1505.07736 [cs, math], May 2015. Keyword(s): calculus, coinduction, Haskell. Abstract:

   Kurz et al. have recently shown that infinite {$\lambda$}-trees with finitely many free variables modulo {$\alpha$}-equivalence form a final coalgebra for a functor on the category of nominal sets. Here we investigate the rational fixpoint of that functor. We prove that it is formed by all rational {$\lambda$}trees, i.e. those {$\lambda$}-trees which have only finitely many subtrees (up to isomorphism). This yields a corecursion principle that allows the definition of operations such as substitution on rational {$\lambda$}-trees.

   [bibtex-key = miliusFinitaryCorecursionInfinitary2015] [bibtex-entry]



3. Abhishek Anand and Ross Knepper. ROSCoq: Robots Powered by Constructive Reals. In Christian Urban and Xingyuan Zhang, editors, Interactive Theorem Proving, volume 9236, pages 34-50. Springer International Publishing, Cham, 2015. ISBN: 978-3-319-22101-4 978-3-319-22102-1. Keyword(s): Coq, reals, verification. Abstract:

   We present ROSCoq, a framework for developing certified Coq programs for robots. ROSCoq subsystems communicate using messages, as they do in the Robot Operating System (ROS). We extend the logic of events to enable holistic reasoning about the cyber-physical behavior of robotic systems. The behavior of the physical world (e.g. Newton's laws) and associated devices (e.g. sensors, actuators) are specified axiomatically. For reasoning about physics we use and extend CoRN's theory of constructive real analysis. Instead of floating points, our Coq programs use CoRN's exact, yet fast computations on reals, thus enabling accurate reasoning about such computations.

   [bibtex-key = anandROSCoqRobotsPowered2015a] [bibtex-entry]



4. Vijay D'Silva and Caterina Urban. Abstract Interpretation as Automated Deduction. In Automated Deduction - CADE-25, Lecture Notes in Computer Science, pages 450-464, August 2015. Springer, Cham. ISBN: 978-3-319-21400-9 978-3-319-21401-6. Keyword(s): abstract interpretation. Abstract:

   Algorithmic deduction and abstract interpretation are two widely used and successful approaches to implementing program verifiers. A major impediment to combining these approaches is that their mathematical foundations and implementation approaches are fundamentally different. This paper presents a new, logical perspective on abstract interpreters that perform reachability analysis using non-relational domains. We encode reachability of a location in a control-flow graph as satisfiability in a monadic, second-order logic parameterized by a first-order theory. We show that three components of an abstract interpreter, the lattice, transformers and iteration algorithm, represent a first-order, substructural theory, parametric deduction and abduction in that theory, and second-order constraint propagation.

   [bibtex-key = dsilvaAbstractInterpretationAutomated2015] [bibtex-entry]



5. Daniel Ricketts, Gregory Malecha, Mario M. Alvarez, Vignesh Gowda, and Sorin Lerner. Towards Verification of Hybrid Systems in a Foundational Proof Assistant. In 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), Austin, TX, USA, pages 248-257, September 2015. IEEE. ISBN: 978-1-5090-0237-5. Keyword(s): verification. Abstract:

   Unsafe behavior of hybrid systems can have disastrous consequences, motivating the need for formal verification of the software running on these systems. Foundational verification in a proof assistant such as Coq is a promising technique that can provide extremely strong, foundational, guarantees about software systems. In this paper, we show how to apply this technique to hybrid systems. We define a TLA-inspired formalism in Coq for reasoning about hybrid systems and use it to verify two quadcopter modules: the first limits the quadcopter's velocity and the second limits its altitude. We ran both of these modules on an actual quadcopter, and they worked as intended. We also discuss lessons learned from our experience foundationally verifying hybrid systems.

   [bibtex-key = rickettsVerificationHybridSystems2015] [bibtex-entry]



6. Martin Lundfall. Formalizing Real Numbers in Agda. , August 2015. Keyword(s): Agda. Abstract:

   With his iconic book Foundations of Constructive Analysis (Bishop and Bridges 1985), Errett Bishop presented the constructive notion of a real number and showed that many of the important theorems of real analysis could be proven without using the law of the excluded middle. This paper aims to show how this notion can be formalized in the dependently typed programming language of Agda. Using the Agda Standard Library (v0.9) and additional work by the GitHub user sabry (Sabry 2014), a major step towards formalizing the de nition of real numbers and the equivalence relation on them is taken. In the process, an alternate de nition of rational numbers in Agda is presented and many important statements on rationals are proven.

   [bibtex-key = lundfallFormalizingRealNumbers2015] [bibtex-entry]

1. Khalil Ghorbal, Jean-Baptiste Jeannin, Erik Zawadzki, André Platzer, Geoffrey J. Gordon, and Peter Capell. Hybrid Theorem Proving of Aerospace Systems: Applications and Challenges. Journal of Aerospace Information Systems, 11(10):702-713, 2014. Keyword(s): avionics, verification. Abstract:

   Complex software systems are becoming increasingly prevalent in aerospace applications: in particular, to accomplish critical tasks. Ensuring the safety of these systems is crucial, as they can have subtly different behaviors under slight variations in operating conditions. This paper advocates the use of formal verification techniques and in particular theorem proving for hybrid software-intensive systems as a well-founded complementary approach to the classical aerospace verification and validation techniques, such as testing or simulation. As an illustration of these techniques, a novel lateral midair collision-avoidance maneuver is studied in an ideal setting, without accounting for the uncertainties of the physical reality. The challenges that naturally arise when applying such technology to industrial-scale applications is then detailed, and proposals are given on how to address these issues.

   [bibtex-key = ghorbalHybridTheoremProving2014] [bibtex-entry]



2. Conor Thomas McBride. How to Keep Your Neighbours in Order. ACM SIGPLAN Notices, 49(9):297-309, November 2014. ISSN: 0362-1340, 1558-1160. Keyword(s): Agda. [bibtex-key = mcbrideHowKeepYour2014] [bibtex-entry]



3. Tobias Nipkow and Gerwin Klein. Abstract Interpretation. In Tobias Nipkow and Gerwin Klein, editors, Concrete Semantics: With Isabelle/HOL, pages 219-280. Springer International Publishing, Cham, 2014. ISBN: 978-3-319-10542-0. Keyword(s): abstract interpretation. Abstract:

   In Chapter 10 we saw a number of automatic program analyses, and each one was hand crafted. Abstract Interpretation is a generic approach to automatic program analysis. In principle, it covers all of our earlier analyses. In this chapter we ignore the optimizing program transformations that accompany certain analyses.

   [bibtex-key = nipkowAbstractInterpretation2014] [bibtex-entry]



4. Gethin Norman and David Parker. Quantitative Verification: Formal Guarantees for Timeliness, Reliability and Performance. Technical report, The London Mathematical Society and the Smith Institute, 2014. Keyword(s): model checking. [bibtex-key = normanQuantitativeVerificationFormal2014] [bibtex-entry]

1. Liya Liu, Osman Hasan, and Sofiène Tahar. Formal Reasoning About Finite-State Discrete-Time Markov Chains in HOL. Journal of Computer Science and Technology, 28(2):217-231, March 2013. ISSN: 1860-4749. Keyword(s): probability, verification. Abstract:

   Markov chains are extensively used in modeling different aspects of engineering and scientific systems, such as performance of algorithms and reliability of systems. Different techniques have been developed for analyzing Markovian models, for example, Markov Chain Monte Carlo based simulation, Markov Analyzer, and more recently probabilistic model-checking. However, these techniques either do not guarantee accurate analysis or are not scalable. Higher-order-logic theorem proving is a formal method that has the ability to overcome the above mentioned limitations. However, it is not mature enough to handle all sorts of Markovian models. In this paper, we propose a formalization of Discrete-Time Markov Chain (DTMC) that facilitates formal reasoning about time-homogeneous finite-state discrete-time Markov chain. In particular, we provide a formal verification on some of its important properties, such as joint probabilities, Chapman-Kolmogorov equation, reversibility property, using higher-order logic. To demonstrate the usefulness of our work, we analyze two applications: a simplified binary communication channel and the Automatic Mail Quality Measurement protocol.

   [bibtex-key = liuFormalReasoningFiniteState2013] [bibtex-entry]



2. Lee Pike, Nis Wegmann, Sebastian Niller, and Alwyn Goodloe. Copilot: Monitoring Embedded Systems. Innovations in Systems and Software Engineering, 9(4):235-255, December 2013. ISSN: 1614-5046, 1614-5054. Keyword(s): Haskell, streams, verification. [bibtex-key = pikeCopilotMonitoringEmbedded2013] [bibtex-entry]

1. Vibhav Gogate and Pedro Domingos. Probabilistic Theorem Proving. arXiv:1202.3724 [cs], February 2012. Keyword(s): probability. Abstract:

   Many representation schemes combining first-order logic and probability have been proposed in recent years. Progress in unifying logical and probabilistic inference has been slower. Existing methods are mainly variants of lifted variable elimination and belief propagation, neither of which take logical structure into account. We propose the first method that has the full power of both graphical model inference and first-order theorem proving (in finite domains with Herbrand interpretations). We first define probabilistic theorem proving, their generalization, as the problem of computing the probability of a logical formula given the probabilities or weights of a set of formulas. We then show how this can be reduced to the problem of lifted weighted model counting, and develop an efficient algorithm for the latter. We prove the correctness of this algorithm, investigate its properties, and show how it generalizes previous approaches. Experiments show that it greatly outperforms lifted variable elimination when logical structure is present. Finally, we propose an algorithm for approximate probabilistic theorem proving, and show that it can greatly outperform lifted belief propagation.

   [bibtex-key = gogateProbabilisticTheoremProving2012] [bibtex-entry]



2. Ugo Dal Lago and Margherita Zorzi. Probabilistic Operational Semantics for the Lambda Calculus. RAIRO - Theoretical Informatics and Applications, 46(3):413-450, July 2012. ISSN: 0988-3754, 1290-385X. Keyword(s): calculus, probability. Abstract:

   Probabilistic operational semantics for a nondeterministic extension of pure {$\lambda$}-calculus is studied. In this semantics, a term evaluates to a (finite or infinite) distribution of values. Small-step and big-step semantics, inductively and coinductively defined, are given. Moreover, small-step and big-step semantics are shown to produce identical outcomes, both in call-by-value and in call-by-name. Plotkin's CPS translation is extended to accommodate the choice operator and shown correct with respect to the operational semantics. Finally, the expressive power of the obtained system is studied: the calculus is shown to be sound and complete with respect to computable probability distributions.

   [bibtex-key = lagoProbabilisticOperationalSemantics2012] [bibtex-entry]



3. Diogo Araújo Carvalho Vilaça Moreira. Finite Probability Distributions in Coq. April 2012. Keyword(s): Coq, probability. Abstract:

   When building safety-critical systems, guaranteeing properties like correctness and security are one of the most important goals to achieve. Thus, from a scientific point of view, one of the hardest problems in cryptography is to build systems whose security properties can be formally demonstrated. In the last few years we have assisted an exponential growth in the use of tools to formalize security proofs of primitives and cryptographic protocols, clearly showing the strong connection between cryptography and formal methods. This necessity comes from the great complexity and sometimes careless presentation of many security proofs, which often contain holes or rely on hidden assumptions that may reveal unknown weaknesses. In this context, interactive theorem provers appear as the perfect tool to aid in the formal certification of programs due to their capability of producing proofs without glitches and providing additional evidence that the proof process is correct. Hence, it is the purpose of this thesis to document the development of a framework for reasoning over information theoretic concepts, which are particularly useful to derive results on the security properties of cryptographic systems. For this it is first necessary to understand, and formalize, the underlying probability theoretic notions. The framework is implemented on top of the fintype and finfun modules of SSREFLECT, which is a small scale reflection extension for the COQ proof assistant, in order to take advantage of the formalization of big operators and finite sets that are available.

   [bibtex-key = moreiraFiniteProbabilityDistributions2012] [bibtex-entry]



4. Paula G. Severi and Fer-Jan J. de Vries. Pure Type Systems with Corecursion on Streams: From Finite to Infinitary Normalisation. ACM SIGPLAN Notices, 47(9):141-152, September 2012. ISSN: 0362-1340. Keyword(s): calculus, coinduction. Abstract:

   In this paper, we use types for ensuring that programs involving streams are well-behaved. We extend pure type systems with a type constructor for streams, a modal operator next and a fixed point operator for expressing corecursion. This extension is called Pure Type Systems with Corecursion (CoPTS). The typed lambda calculus for reactive programs defined by Krishnaswami and Benton can be obtained as a CoPTS. CoPTSs allow us to study a wide range of typed lambda calculi extended with corecursion using only one framework. In particular, we study this extension for the calculus of constructions which is the underlying formal language of Coq. We use the machinery of infinitary rewriting and formalise the idea of well-behaved programs using the concept of infinitary normalisation. The set of finite and infinite terms is defined as a metric completion. We establish a precise connection between the modal operator ( extbullet{} A) and the metric at a syntactic level by relating a variable of type ( extbullet{} A) with the depth of all its occurrences in a term. This syntactic connection between the modal operator and the depth is the key to the proofs of infinitary weak and strong normalisation.

   [bibtex-key = severiPureTypeSystems2012] [bibtex-entry]

1. Sergey Goncharov and Lutz Schröder. A Coinductive Calculus for Asynchronous Side-Effecting Processes. arXiv:1104.2936 [cs], April 2011. Keyword(s): asynchronous, calculus. Abstract:

   We present an abstract framework for concurrent processes in which atomic steps have generic side effects, handled according to the principle of monadic encapsulation of effects. Processes in this framework are potentially infinite resumptions, modelled using final coalgebras over the monadic base. As a calculus for such processes, we introduce a concurrent extension of Moggi's monadic metalanguage of effects. We establish soundness and completeness of a natural equational axiomatisation of this calculus. Moreover, we identify a corecursion scheme that is explicitly definable over the base language and provides flexible expressive means for the definition of new operators on processes, such as parallel composition. As a worked example, we prove the safety of a generic mutual exclusion scheme using a verification logic built on top of the equational calculus.

   [bibtex-key = goncharovCoinductiveCalculusAsynchronous2011] [bibtex-entry]



2. Osman Hasan and Sofiène Tahar. Reasoning about Conditional Probabilities in a Higher-Order-Logic Theorem Prover. Journal of Applied Logic, 9(1):23-40, March 2011. ISSN: 1570-8683. Keyword(s): HOL, probability. Abstract:

   In the field of probabilistic analysis, the concept of conditional probability plays a major role for estimating probabilities when some partial information concerning the result of the experiment is available. This paper presents a higher-order-logic definition of conditional probability and the formal verification of some classical properties of conditional probability, such as, the total probability law and Bayes' theorem. This infrastructure, implemented in the HOL theorem prover, allows us to precisely reason about conditional probabilities for probabilistic systems within the sound core of HOL and thus proves to be quite useful for the analysis of systems used in safety-critical domains, such as space, medicine and transportation. To demonstrate the usefulness of our approach, we provide the precise probabilistic analysis of the binary asymmetric channel, a widely used concept in communication theory, within the HOL theorem prover.

   [bibtex-key = hasanReasoningConditionalProbabilities2011] [bibtex-entry]



3. Ugo Dal Lago and Margherita Zorzi. Probabilistic Operational Semantics for the Lambda Calculus. arXiv:1104.0195 [cs], June 2011. Keyword(s): calculus, probability. Abstract:

   Probabilistic operational semantics for a nondeterministic extension of pure lambda calculus is studied. In this semantics, a term evaluates to a (finite or infinite) distribution of values. Small-step and big-step semantics are both inductively and coinductively defined. Moreover, small-step and big-step semantics are shown to produce identical outcomes, both in call-by- value and in call-by-name. Plotkin's CPS translation is extended to accommodate the choice operator and shown correct with respect to the operational semantics. Finally, the expressive power of the obtained system is studied: the calculus is shown to be sound and complete with respect to computable probability distributions.

   [bibtex-key = lagoProbabilisticOperationalSemantics2011] [bibtex-entry]



4. Vojtech Forejt, Marta Kwiatkowska, Gethin Norman, and David Parker. Automated Verification Techniques for Probabilistic Systems. In Marco Bernardo and Valérie Issarny, editors, Formal Methods for Eternal Networked Software Systems, volume 6659, pages 53-113. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011. ISBN: 978-3-642-21454-7 978-3-642-21455-4. Keyword(s): probability, verification. Abstract:

   This tutorial provides an introduction to probabilistic model checking, a technique for automatically verifying quantitative properties of probabilistic systems. We focus on Markov decision processes (MDPs), which model both stochastic and nondeterministic behaviour. We describe methods to analyse a wide range of their properties, including specifications in the temporal logics PCTL and LTL, probabilistic safety properties and cost- or reward-based measures. We also discuss multiobjective probabilistic model checking, used to analyse trade-offs between several different quantitative properties. Applications of the techniques in this tutorial include performance and dependability analysis of networked systems, communication protocols and randomised distributed algorithms. Since such systems often comprise several components operating in parallel, we also cover techniques for compositional modelling and verification of multi-component probabilistic systems. Finally, we describe three large case studies which illustrate practical applications of the various methods discussed in the tutorial.

   [bibtex-key = forejtAutomatedVerificationTechniques2011] [bibtex-entry]

1. Ralf Hinze. Concrete Stream Calculus: An Extended Study. Journal of Functional Programming, 20(5-6):463-535, November 2010. ISSN: 0956-7968, 1469-7653. Keyword(s): coinduction, Haskell. Abstract:

   This paper shows how to reason about streams concisely and precisely. Streams, infinite sequences of elements, live in a coworld: they are given by a coinductive datatype, operations on streams are implemented by corecursive programs, and proofs are typically concocted using coinduction. This paper offers an alternative to coinduction. Suitably restricted, stream equations possess unique solutions. This property gives rise to a simple and attractive proof technique, essentially bringing equational reasoning to the coworld. We redevelop the theory of recurrences, finite calculus and generating functions using streams and stream operators, building on the cornerstone of unique solutions. The paper contains a smo extasciidieresis rg\r{}asbord of examples: we study recursion elimination, investigate the binary carry sequence, explore Sprague-Grundy numbers and present two proofs of Moessner's Theorem. The calculations benefit from the rich structure of streams. As the type of streams is an applicative functor we can effortlessly lift operations and their properties to streams. In combination with Haskell's facilities for overloading, this greatly contributes to conciseness of notation. The development is indeed constructive: streams and stream operators are implemented in Haskell, usually by one-liners. The resulting calculus or library, if you wish, is elegant and fun to use.

   [bibtex-key = hinzeConcreteStreamCalculus2010] [bibtex-entry]



2. Taylor. A Lambda Calculus for Real Analysis. Journal of Logic and Analysis, 2010. ISSN: 17599008. Keyword(s): calculus, reals. Abstract:

   Abstract Stone Duality is a new paradigm for general topology in which computable continuous functions are described directly, without using set theory, infinitary lattice theory or a prior theory of discrete computation. Every expression in the calculus denotes both a continuous function and a program, and the reasoning looks remarkably like a sanitised form of that in classical topology. This is an introduction to ASD for the general mathematician, with application to elementary real analysis.

   [bibtex-key = taylorLambdaCalculusReal2010] [bibtex-entry]

1. Daphne Koller and Nir Friedman. Probabilistic Graphical Models: Principles and Techniques. MIT press, 2009. Keyword(s): probability. [bibtex-key = kollerProbabilisticGraphicalModels2009] [bibtex-entry]



2. Osman Hasan and Sofiène Tahar. Formal Verification of Tail Distribution Bounds in the HOL Theorem Prover. Mathematical Methods in the Applied Sciences, 32(4):480-504, March 2009. ISSN: 01704214, 10991476. Keyword(s): HOL, probability. Abstract:

   Tail distribution bounds play a major role in the estimation of failure probabilities in performance and reliability analysis of systems. They are usually estimated using Markov's and Chebyshev's inequalities, which represent tail distribution bounds for a random variable in terms of its mean or variance. This paper presents the formal verification of Markov's and Chebyshev's inequalities for discrete random variables using a higher-order-logic theorem prover. The paper also provides the formal verification of mean and variance relations for some of the widely used discrete random variables, such as Uniform(m), Bernoulli( p), Geometric( p) and Binomial(m, p) random variables. This infrastructure allows us to precisely reason about the tail distribution properties and thus turns out to be quite useful for the analysis of systems used in safety-critical domains, such as space, medicine or transportation. For illustration purposes, we present the performance analysis of the coupon collector's problem, a well-known commercially used algorithm. Copyright q 2008 John Wiley \& Sons, Ltd.

   [bibtex-key = hasanFormalVerificationTail2009] [bibtex-entry]



3. Osman Hasan and Sofiène Tahar. Probabilistic Analysis of Wireless Systems Using Theorem Proving. Electronic Notes in Theoretical Computer Science, 242(2):43-58, July 2009. ISSN: 15710661. Keyword(s): HOL, probability. Abstract:

   Probabilistic techniques play a major role in the design and analysis of wireless systems as they contain a significant amount of random or unpredictable components. Traditionally, computer simulation techniques are used to perform probabilistic analysis of wireless systems but they provide inaccurate results and usually require enormous amount of CPU time in order to attain reasonable estimates. To overcome these limitations, we propose to use a higher-order-logic theorem prover (HOL) for the analysis of wireless systems. The paper presents a concise description of the formal foundations required to conduct the analysis of a wireless system in a theorem prover, such as the higher-order-logic modeling of random variables and the verification of their corresponding probabilistic and statistical properties in a theorem prover. In order to illustrate the utilization and effectiveness of the proposed idea for handling real-world wireless system analysis problems, we present an analysis of the automated repeat request (ARQ) mechanism at the logic link control (LLC) layer of the General Packet Radio Service (GPRS), which is a packet oriented mobile data service available to the users of Global System for Mobile Communications (GSM).

   [bibtex-key = hasanProbabilisticAnalysisWireless2009] [bibtex-entry]



4. Favio Ezequiel Miranda-Perea. Two Extensions of System F with (Co)Iteration and Primitive (Co)Recursion Principles. RAIRO - Theoretical Informatics and Applications, 43(4):703-766, October 2009. ISSN: 0988-3754, 1290-385X. Keyword(s): calculus, coinduction. Abstract:

   This paper presents two extensions of the second order polymorphic lambda calculus, system F, with monotone (co)inductive types supporting (co)iteration, primitive (co)recursion and inversion principles as primitives. One extension is inspired by the usual categorical approach to programming by means of initial algebras and final coalgebras; whereas the other models dialgebras, and can be seen as an extension of Hagino's categorical lambda calculus within the framework of parametric polymorphism. The systems are presented in Curry-style, and are proven to be terminating and type-preserving. Moreover their expressiveness is shown by means of several programming examples, going from usual data types to lazy codata types such as streams or infinite trees.

   [bibtex-key = miranda-pereaTwoExtensionsSystem2009] [bibtex-entry]

1. Osman Hasan. Formal Probabilistic Analysis Using Theorem Proving. PhD Thesis, Concordia University, Montréal, Canada, April 2008. Keyword(s): HOL, probability. [bibtex-key = hasanFormalProbabilisticAnalysis2008] [bibtex-entry]



2. Stephen J. Fink, Eran Yahav, Nurit Dor, G. Ramalingam, and Emmanuel Geay. Effective Typestate Verification in the Presence of Aliasing. ACM Transactions on Software Engineering and Methodology, 17(2):1-34, April 2008. ISSN: 1049-331X, 1557-7392. Keyword(s): abstract interpretation. [bibtex-key = finkEffectiveTypestateVerification2008] [bibtex-entry]



3. Osman Hasan and Sofiène Tahar. Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables. Journal of Automated Reasoning, 41(3-4):295-323, November 2008. ISSN: 0168-7433, 1573-0670. Keyword(s): HOL, probability. Abstract:

   Statistical quantities, such as expectation (mean) and variance, play a vital role in the present age probabilistic analysis. In this paper, we present some formalization of expectation theory that can be used to verify the expectation and variance characteristics of discrete random variables within the HOL theorem prover. The motivation behind this is the ability to perform error free probabilistic analysis, which in turn can be very useful for the performance and reliability analysis of systems used in safety-critical domains, such as space travel, medicine and military. We first present a formal definition of expectation of a function of a discrete random variable. Building upon this definition, we formalize the mathematical concept of variance and verify some classical properties of expectation and variance in HOL. We then utilize these formal definitions to verify the expectation and variance characteristics of the Geometric random variable. In order to demonstrate the practical effectiveness of the formalization presented in this paper, we also present the probabilistic analysis of the Coupon Collector's problem in HOL.

   [bibtex-key = hasanUsingTheoremProving2008] [bibtex-entry]



4. André Platzer. Differential Dynamic Logic for Hybrid Systems. Journal of Automated Reasoning, 41(2):143-189, August 2008. ISSN: 1573-0670. Keyword(s): verification. Abstract:

   Hybrid systems are models for complex physical systems and are defined as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. With the goal of developing a theoretical and practical foundation for deductive verification of hybrid systems, we introduce a dynamic logic for hybrid programs, which is a program notation for hybrid systems. As a verification technique that is suitable for automation, we introduce a free variable proof calculus with a novel combination of real-valued free variables and Skolemisation for lifting quantifier elimination for real arithmetic to dynamic logic. The calculus is compositional, i.e., it reduces properties of hybrid programs to properties of their parts. Our main result proves that this calculus axiomatises the transition behaviour of hybrid systems completely relative to differential equations. In a case study with cooperating traffic agents of the European Train Control System, we further show that our calculus is well-suited for verifying realistic hybrid systems with parametric system dynamics.

   [bibtex-key = platzerDifferentialDynamicLogic2008] [bibtex-entry]



5. J. J. M. M. Rutten. Rational Streams Coalgebraically. Logical Methods in Computer Science, 4(3):9, September 2008. ISSN: 18605974. Keyword(s): streams. Abstract:

   We study rational streams (over a field) from a coalgebraic perspective. Exploiting the finality of the set of streams, we present an elementary and uniform proof of the equivalence of four notions of representability of rational streams: by finite dimensional linear systems; by finite stream circuits; by finite weighted stream automata; and by finite dimensional subsystems of the set of streams.

   [bibtex-key = ruttenRationalStreamsCoalgebraically2008] [bibtex-entry]

1. Ulf Norell. Towards a Practical Programming Language Based on Dependent Type Theory. PhD Thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden, September 2007. Keyword(s): Agda. Abstract:

   Dependent type theories [ML72] have a long history of being used for theorem proving. One aspect of type theory which makes it very powerful as a proof language is that it mixes deduction with computation. This also makes type theory a good candidate for programming extemdash the strength of the type system allows properties of programs to be stated and established, and the computational properties provide semantics for the programs.

   [bibtex-key = norellPracticalProgrammingLanguage2007] [bibtex-entry]



2. Yannick Moy and Claude Marché. Inferring Local (Non-) Aliasing and Strings for Memory Safety. Heap Analysis and Verification (HAV'07), pp 35-51, 2007. Keyword(s): abstract interpretation. [bibtex-key = moyInferringLocalNon2007] [bibtex-entry]



3. Sumit Gulwani and Ashish Tiwari. An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software. In Werner Damm and Holger Hermanns, editors, Computer Aided Verification, volume 4590, pages 379-392. Springer Berlin Heidelberg, Berlin, Heidelberg, 2007. ISBN: 978-3-540-73367-6. Keyword(s): abstract interpretation. [bibtex-key = gulwaniAbstractDomainAnalyzing2007] [bibtex-entry]



4. Osman Hasan and Sofiène Tahar. Formalization of Continuous Probability Distributions. In Frank Pfenning, editor, Automated Deduction - CADE-21, volume 4603, pages 3-18. Springer Berlin Heidelberg, Berlin, Heidelberg, 2007. ISBN: 978-3-540-73594-6 978-3-540-73595-3. ISSN: 0302-9743, 1611-3349. Keyword(s): HOL, probability. Abstract:

   In order to overcome the limitations of state-of-the-art simulation based probabilistic analysis, we propose to perform probabilistic analysis within the environment of a higher-order-logic theorem prover. The foremost requirement for conducting such analysis is the formalization of probability distributions. In this report, we present a methodology for the formalization of continuous probability distributions for which the inverse of the cumulative distribution function can be expressed in a closed mathematical form. Our methodology is primarily based on the formalization of the Standard Uniform random variable, cumulative distribution function properties and the Inverse Transform method. The report presents all this formalization using the HOL theorem prover. In order to illustrate the practical effectiveness of our methodology, the formalization of a few continuous probability distributions has also been included.

   [bibtex-key = hasanFormalizationContinuousProbability2007] [bibtex-entry]

1. Gul Agha, José Meseguer, and Koushik Sen. PMaude: Rewrite-Based Specification Language for Probabilistic Object Systems. Electronic Notes in Theoretical Computer Science, 153(2):213-239, May 2006. ISSN: 1571-0661. Keyword(s): actors, asynchronous, probability. Abstract:

   We introduce a rewrite-based specification language for modelling probabilistic concurrent and distributed systems. The language, based on PMaude, has both a rigorous formal basis and the characteristics of a high-level rule-based programming language. Furthermore, we provide tool support for performing discrete-event simulations of models written in PMaude, and for statistically analyzing various quantitative aspects of such models based on the samples that are generated through discrete-event simulation. Because distributed and concurrent communication protocols can be modelled using actors (concurrent objects with asynchronous message passing), we provide an actor PMaude module. The module aids writing specifications in a probabilistic actor formalism. This allows us to easily write specifications that are purely probabilistic extendash{} and not just non-deterministic. The absence of such (un-quantified) non-determinism in a probabilistic system is necessary for a form of statistical analysis that we also discuss. Specifically, we introduce a query language called Quantitative Temporal Expressions (or QuaTEx in short), to query various quantitative aspects of a probabilistic model. We also describe a statistical technique to evaluate QuaTEx expressions for a probabilistic model.

   [bibtex-key = aghaPMaudeRewritebasedSpecification2006] [bibtex-entry]



2. Alberto Ciaffaglione and Pietro Di Gianantonio. A Certified, Corecursive Implementation of Exact Real Numbers. Theoretical Computer Science, 351(1):39-51, February 2006. ISSN: 0304-3975. Keyword(s): Coq, reals. Abstract:

   We implement exact real numbers in the logical framework Coq using streams, i.e., infinite sequences, of digits, and characterize constructive real numbers through a minimal axiomatization. We prove that our construction inhabits the axiomatization, working formally with coinductive types and corecursive proofs. Thus we obtain reliable, corecursive algorithms for computing on real numbers.

   [bibtex-key = ciaffaglioneCertifiedCorecursiveImplementation2006] [bibtex-entry]



3. Antoine Miné. The Octagon Abstract Domain. Higher-Order and Symbolic Computation, 19(1):31-100, March 2006. ISSN: 1573-0557. Keyword(s): abstract interpretation. Abstract:

   This article presents the octagon abstract domain, a relational numerical abstract domain for static analysis by abstract interpretation. It allows representing conjunctions of constraints of the form {$\pm$} X {$\pm$} Y {$\leq$} c where X and Y range among program variables and c is a constant in {$\mathbb{Z}$}, {$\mathbb{Q}$}, or {$\mathbb{R}$} automatically inferred. Abstract elements are represented using modified Difference Bound Matrices and we use a normalization algorithm loosely based on the shortest-path closure to compute canonical representations and construct best-precision abstract transfer functions. We achieve a quadratic memory cost per abstract element and a cubic worst-case time cost per abstract operation, with respect to the number of program variables.

   [bibtex-key = mineOctagonAbstractDomain2006] [bibtex-entry]



4. Peter Selinger and Benoit Valiron. A Lambda Calculus for Quantum Computation with Classical Control. Mathematical Structures in Computer Science, 16(3):527-552, June 2006. ISSN: 0960-1295. Keyword(s): calculus, quantum. Abstract:

   In this paper we develop a functional programming language for quantum computers by extending the simply-typed lambda calculus with quantum types and operations. The design of this language adheres to the `quantum data, classical control' paradigm, following the first author's work on quantum flow-charts. We define a call-by-value operational semantics, and give a type system using affine intuitionistic linear logic. The main results of this paper are the safety properties of the language and the development of a type inference algorithm.

   [bibtex-key = selingerLambdaCalculusQuantum2006] [bibtex-entry]



5. Andrew Hinton, Marta Kwiatkowska, Gethin Norman, and David Parker. PRISM: A Tool for Automatic Verification of Probabilistic Systems. In Holger Hermanns and Jens Palsberg, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 3920, pages 441-444. Springer Berlin Heidelberg, Berlin, Heidelberg, 2006. ISBN: 978-3-540-33056-1 978-3-540-33057-8. Keyword(s): model checking, probability. Abstract:

   Probabilistic model checking is an automatic formal verification technique for analysing quantitative properties of systems which exhibit stochastic behaviour. PRISM is a probabilistic model checking tool which has already been successfully deployed in a wide range of application domains, from real-time communication protocols to biological signalling pathways. The tool has recently undergone a significant amount of development. Major additions include facilities to manually explore models, Monte-Carlo discrete-event simulation techniques for approximate model analysis (including support for distributed simulation) and the ability to compute cost- and reward-based measures, e.g. ``the expected energy consumption of the system before the first failure occurs''. This paper presents an overview of all the main features of PRISM. More information can be found on the website: www.cs.bham.ac.uk/ exttildelow dxp/prism.

   [bibtex-key = hintonPRISMToolAutomatic2006] [bibtex-entry]



6. Osman Hasan and Sofiene Tahar. Formalization of the Standard Uniform Random Variable in HOL. Technical report, December 2006. Keyword(s): HOL, probability. Abstract:

   Continuous random variables are widely used to mathematically describe random phenomenon in engineering and physical sciences. In this paper, we present a higher-order logic formalization of the Standard Uniform random variable. We show the correctness of this specification by proving the corresponding probability distribution properties within the HOL theorem prover and the proof steps have been summarized. This formalized Standard Uniform random variable can be transformed to formalize other continuous random variables, such as Uniform, Exponential, Normal, etc., by using various Non-uniform random number generation techniques. The formalization of these continuous random variables will enable us to perform error free probabilistic analysis of systems within the framework of a higher-order-logic theorem prover. For illustration purposes, we present the formalization of the Continuous Uniform random variable based on our Standard Uniform random variable and then utilize it to perform a simple probabilistic analysis of roundoff error in HOL.

   [bibtex-key = hasanFormalizationStandardUniform2006] [bibtex-entry]

1. Wilfried Buchholz. A Term Calculus for (Co-)Recursive Definitions on Streamlike Data Structures. Annals of Pure and Applied Logic, 136(1):75-90, October 2005. ISSN: 0168-0072. Keyword(s): calculus, streams. Abstract:

   We introduce a system of simply typed lambda terms (with fixed point combinators) and show that a rather comprehensive class of (co-)recursion equations on streams or non-wellfounded trees can be solved in our system. Moreover certain conditions are presented which guarantee that the defined functionals are primitive recursive. As a major example we give a co-recursive treatment of Mints' continuous cut-elimination operator.

   [bibtex-key = buchholzTermCalculusCo2005] [bibtex-entry]



2. Koushik Sen, Mahesh Viswanathan, and Gul Agha. On Statistical Model Checking of Stochastic Systems. In David Hutchison, Takeo Kanade, Josef Kittler, Jon M. Kleinberg, Friedemann Mattern, John C. Mitchell, Moni Naor, Oscar Nierstrasz, C. Pandu Rangan, Bernhard Steffen, Madhu Sudan, Demetri Terzopoulos, Dough Tygar, Moshe Y. Vardi, Gerhard Weikum, Kousha Etessami, and Sriram K. Rajamani, editors, Computer Aided Verification, volume 3576, pages 266-280. Springer Berlin Heidelberg, Berlin, Heidelberg, 2005. ISBN: 978-3-540-27231-1 978-3-540-31686-2. Keyword(s): model checking, probability. Abstract:

   Statistical methods to model check stochastic systems have been, thus far, developed only for a sublogic of continuous stochastic logic (CSL) that does not have steady state operator and unbounded until formulas. In this paper, we present a statistical model checking algorithm that also verifies CSL formulas with unbounded untils. The algorithm is based on Monte Carlo simulation of the model and hypothesis testing of the samples, as opposed to sequential hypothesis testing. We have implemented the algorithm in a tool called VESTA, and found it to be effective in verifying several examples.

   [bibtex-key = senStatisticalModelChecking2005] [bibtex-entry]



3. K. Sen, M. Viswanathan, and G. Agha. VESTA: A Statistical Model-Checker and Analyzer for Probabilistic Systems. In Second International Conference on the Quantitative Evaluation of Systems (QEST'05), Torino, Italy, pages 251-252, 2005. IEEE. ISBN: 978-0-7695-2427-6. Keyword(s): model checking, probability. Abstract:

   We give a brief overview of a statistical model-checking and analysis tool VESTA. 1 Overview of VESTA VESTA is a tool for statistical analysis of probabilistic systems. It supports statistical model-checking [5, 6] and statistical evaluation of expected values of temporal expressions. For model-checking VESTA uses a sequence of inter-related statistical hypothesis testing to check if a property specified in probabilistic computation tree logic (PCTL) [2] or continuous stochastic logic (CSL) is satisfied by a stochastic model. Furthermore, VESTA supports the statistical computation of expected values of expressions written in a query language called Quantitative Temporal Expressions (or QUATEX in short). We next describe the various components of the tool.

   [bibtex-key = senVESTAStatisticalModelchecker2005] [bibtex-entry]

1. Antoine Miné. Weakly Relational Numerical Abstract Domains. PhD Thesis, Ecole Polytechnique X, 2004. Keyword(s): abstract interpretation. [bibtex-key = mineWeaklyRelationalNumerical2004] [bibtex-entry]



2. Patrick Cousot and Radhia Cousot. An Abstract Interpretation-Based Framework for Software Watermarking. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '04, New York, NY, USA, pages 173-185, 2004. ACM. ISBN: 978-1-58113-729-3. Keyword(s): abstract interpretation. Abstract:

   Software watermarking consists in the intentional embedding of indelible stegosignatures or watermarks into the subject software and extraction of the stegosignatures embedded in the stegoprograms for purposes such as intellectual property protection. We introduce the novel concept of abstract software watermarking. The basic idea is that the watermark is hidden in the program code in such a way that it can only be extracted by an abstract interpretation of the (maybe non-standard) concrete semantics of this code. This static analysis-based approach allows the watermark to be recovered even if only a small part of the program code is present and does not even need that code to be executed. We illustrate the technique by a simple abstract watermarking protocol for methods of Java exttrademark{} classes. The concept applies equally well to any other kind of software (including hardware originally specified by software).

   [bibtex-key = cousotAbstractInterpretationbasedFramework2004] [bibtex-entry]

1. Thomas Ehrhard and Laurent Regnier. The Differential Lambda-Calculus. Theoretical Computer Science, 309(1):1-41, December 2003. ISSN: 0304-3975. Keyword(s): calculus. Abstract:

   We present an extension of the lambda-calculus with differential constructions. We state and prove some basic results (confluence, strong normalization in the typed case), and also a theorem relating the usual Taylor series of analysis to the linear head reduction of lambda-calculus.

   [bibtex-key = ehrhardDifferentialLambdacalculus2003] [bibtex-entry]



2. Joe Hurd. Formal Verification of Probabilistic Algorithms. Technical report UCAM-CL-TR-566, University of Cambridge, Computer Laboratory, May 2003. Keyword(s): probability, verification. [bibtex-key = hurdFormalVerificationProbabilistic2003] [bibtex-entry]

1. Norman Ramsey and Avi Pfeffer. Stochastic Lambda Calculus and Monads of Probability Distributions. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '02, Portland, Oregon, pages 154-165, January 2002. Association for Computing Machinery. ISBN: 978-1-58113-450-6. Keyword(s): calculus, probability. Abstract:

   Probability distributions are useful for expressing the meanings of probabilistic languages, which support formal modeling of and reasoning about uncertainty. Probability distributions form a monad, and the monadic definition leads to a simple, natural semantics for a stochastic lambda calculus, as well as simple, clean implementations of common queries. But the monadic implementation of the expectation query can be much less efficient than current best practices in probabilistic modeling. We therefore present a language of measure terms, which can not only denote discrete probability distributions but can also support the best known modeling techniques. We give a translation of stochastic lambda calculus into measure terms. Whether one translates into the probability monad or into measure terms, the results of the translations denote the same probability distribution.

   [bibtex-key = ramseyStochasticLambdaCalculus2002] [bibtex-entry]

1. J. J. M. M. Rutten. Elements of Stream Calculus: (An Extensive Exercise in Coinduction). Electronic Notes in Theoretical Computer Science, 45:358-423, November 2001. ISSN: 1571-0661. Keyword(s): reals, streams. Abstract:

   Based on the presence of a final coalgebra structure on the set of streams (infinite sequences of real numbers), a coinductive calculus of streams is developed. The main ingredient is the notion of stream derivative, with which both coinductive proofs and definitions can be formulated. In close analogy to classical analysis, the latter are presented as behavioural differential equations. A number of applications of the calculus are presented, including difference equations, analytical differential equations, continued fractions, and some problems from discrete mathematics and combinatorics.

   [bibtex-key = ruttenElementsStreamCalculus2001] [bibtex-entry]



2. Patrick Cousot. Abstract Interpretation Based Formal Methods and Future Challenges. In Informatics, pages 138-156, 2001. Springer. Keyword(s): abstract interpretation. [bibtex-key = cousotAbstractInterpretationBased2001] [bibtex-entry]

1. Oltea Mihaela Herescu and Catuscia Palamidessi. Probabilistic Asynchronous $\pi$-Calculus. In Jerzy Tiuryn, editor, Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, Berlin, Heidelberg, pages 146-160, 2000. Springer. ISBN: 978-3-540-46432-7. Keyword(s): pi calculus, calculus, probability. Abstract:

   We propose an extension of the asynchronous {$\pi$}-calculus with a notion of random choice. We define an operational semantics which distinguishes between probabilistic choice, made internally by the process, and nondeterministic choice, made externally by an adversary scheduler. This distinction will allow us to reason about the probabilistic correctness of algorithms under certain schedulers. We show that in this language we can solve the electoral problem, which was proved not possible in the asynchronous {$\pi$}-calculus. Finally, we show an implementation of the probabilistic asynchronous {$\pi$}-calculus in a Java-like language.

   [bibtex-key = herescuProbabilisticAsynchronousPCalculus2000] [bibtex-entry]

1. Luca de Alfaro. Formal Verification of Probabilistic Systems. PhD Thesis, Standford University, Standford, USA, 1997. Keyword(s): probability, verification. [bibtex-key = dealfaroFormalVerificationProbabilistic1997] [bibtex-entry]



2. Lawrence C. Paulson. Mechanizing Coinduction and Corecursion in Higher-Order Logic. Journal of Logic and Computation, 7(2):175-204, April 1997. ISSN: 0955-792X. Keyword(s): coinduction, HOL. Abstract:

   Abstract. A theory of recursive and corecursive definitions has been developed in higher-order logic (HOL) and mechanized using Isabelle. Least fixedpoints exp

   [bibtex-key = paulsonMechanizingCoinductionCorecursion1997] [bibtex-entry]

1. Arnaud Venet. Abstract Cofibered Domains: Application to the Alias Analysis of Untyped Programs. In Gerhard Goos, Juris Hartmanis, Jan van Leeuwen, Radhia Cousot, and David A. Schmidt, editors, Static Analysis, volume 1145, pages 366-382. Springer Berlin Heidelberg, Berlin, Heidelberg, 1996. ISBN: 978-3-540-61739-6 978-3-540-70674-8. Keyword(s): abstract interpretation. [bibtex-key = venetAbstractCofiberedDomains1996] [bibtex-entry]

1. François Bourdoncle. Interprocedural Abstract Interpretation of Block Structured Languages with Nested Procedures, Aliasing and Recursivity. In Pierre Deransart and Jan Maluszynski, editors, Programming Language Implementation and Logic Programming, Lecture Notes in Computer Science, Berlin, Heidelberg, pages 307-323, 1990. Springer. ISBN: 978-3-540-46298-9. Keyword(s): abstract interpretation. [bibtex-key = bourdoncleInterproceduralAbstractInterpretation1990a] [bibtex-entry]



2. François Bourdoncle. Interprocedural Abstract Interpretation of Block Structured Languages with Nested Procedures, Aliasing and Recursivity. In Pierre Deransart and Jan Maluszynski, editors, Programming Language Implementation and Logic Programming, Lecture Notes in Computer Science, pages 307-323, 1990. Springer Berlin Heidelberg. ISBN: 978-3-540-46298-9. Keyword(s): abstract interpretation. [bibtex-key = bourdoncleInterproceduralAbstractInterpretation1990] [bibtex-entry]



3. Alan Deutsch. On Determining Lifetime and Aliasing of Dynamically Allocated Data in Higher-Order Functional Specifications. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL '90, San Francisco, California, United States, pages 157-168, 1990. ACM Press. ISBN: 978-0-89791-343-0. Keyword(s): abstract interpretation. [bibtex-key = deutschDeterminingLifetimeAliasing1990] [bibtex-entry]

1. Patrick Cousot and Radhia Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL '77, New York, NY, USA, pages 238-252, 1977. ACM. Keyword(s): abstract interpretation. Abstract:

   A program denotes computations in some universe of objects. Abstract interpretation of programs consists in using that denotation to describe computations in another universe of abstract objects, so that the results of abstract execution give some information on the actual computations. An intuitive example (which we borrow from Sintzoff [72]) is the rule of signs. The text -1515 * 17 may be understood to denote computations on the abstract universe (+), (-), (+-) where the semantics of arithmetic operators is defined by the rule of signs. The abstract execution -1515 * 17 extrightarrow{} -(+) * (+) extrightarrow{} (-) * (+) extrightarrow{} (-), proves that -1515 * 17 is a negative number. Abstract interpretation is concerned by a particular underlying structure of the usual universe of computations (the sign, in our example). It gives a summary of some facets of the actual executions of a program. In general this summary is simple to obtain but inaccurate (e.g. -1515 + 17 extrightarrow{} -(+) + (+) extrightarrow{} (-) + (+) extrightarrow{} ({$\pm$})). Despite its fundamentally incomplete results abstract interpretation allows the programmer or the compiler to answer questions which do not need full knowledge of program executions or which tolerate an imprecise answer, (e.g. partial correctness proofs of programs ignoring the termination problems, type checking, program optimizations which are not carried in the absence of certainty about their feasibility, ...).

   [bibtex-key = cousotAbstractInterpretationUnified1977] [bibtex-entry]

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