13th International Symposium on Automated Technology for Verification and Analysis
October 12–15, 2015, Shanghai, China
Computer hardware and software can be modeled precisely in mathematical logic. If expressed appropriately, these models can be executable, i.e., run on concrete data. This allows them to be used as simulation engines or rapid prototypes. But because they are formal they can be manipulated by symbolic means: theorems can be proved about them, directly, with mechanical theorem provers. But how practical is this vision of machines reasoning about machines? In this highly personal talk, I will describe the 45 year history of the "Boyer-Moore theorem prover", starting with its use in Edinburgh, Scotland, to prove simple list processing theorems by mathematical induction (e.g., the reverse of the reverse of x is x) to its routine commercial use in the microprocessor industry (e.g., the floating point operations of the Via Nano 64-bit X86 microprocessor are compliant with the IEEE standard). Along the way we will see applications in program verification, models of instruction set architectures including the JVM, and security and information flow. I then list some reasons this project has been successful. The paper also serves as an annotated bibliography of the key stepping stones in the applications of the prover.
For organisations like Facebook, high quality software is important. However, the pace of change and increasing complexity of modern code makes it difficult to produce error-free software. Available tools are often lacking in helping programmers develop more reliable and secure applications. Formal verification is a technique able to detect software errors statically, before a product is actually shipped. Although this aspect makes this technology very appealing in principle, in practice there have been many difficulties that have hindered the application of software verification in industrial environments. In particular, in an organisation like Facebook where the release cycle is fast compared to more traditional industries, the deployment of formal techniques is highly challenging. In this talk we describe our experience in integrating a verification tool based on static analysis into the software development cycle at Facebook.
Probabilistic programs are sequential programs with two added features: (1) the ability to draw values at random from (possibly parametric) probability distributions, and (2) the ability to condition values of variables in a program through observations. In this talk, I will address the following elementary issues of probabilistic programs: what do they mean?, how to determine loop invariants?, how to analyse parametric programs?, and how hard is it to prove that a program almost surely terminates, i.e., terminates with probability one?
In this tutorial I will use ACL2 interactively to formalize several simple problems and to prove theorems about those formalizations. I will structure the demonstrations so that students will see how a normal user figures out how to help ACL2 find proofs that it cannot find entirely automatically.
Cyber-physical systems are characterized by, first and foremost, featuring a tight interaction between their computational and physical components, but add aspects of networking, distributed control, mobility, autonomy, cooperation, integration with IT-services ("internet of things"), and human-machine interaction to this. Bringing all kinds of physical processes, even geographically or otherwise remote ones, into the sphere of our control, cyber-physical systems transfer the familiar ease of interfacing with the virtual world to the physical world and will thus fundamentally change the way we interact with our environment. Interacting via traditional human-computer interfaces, e.g. through smartphone GUIs, and substituting classical controls, e.g. in remotely controlling household appliances, are just the small beginnings; future applications will inevitably offer more diverse, direct, and partially subconscious user interfaces, they will extend the sphere of control from isolated facets and clearly localized physical items to global networking, and they will rapidly grow in criticality, inducing a societal dependency on continued availability and correct function of the systems. While they do provide a natural next step in an evolution from embedded systems over hybrid systems to a world seamlessly integrating physical and virtual entities with each other and with human cognition, cyber-physical systems thus confront system design and analysis with new challenges: missions and system boundaries will be less well-defined in advance, emergent behavior within dynamically forming, unforeseen cooperative group becomes the rule, and long-term autonomy facilitating systems to survive in an unattended and unsupervised manner for orders of magnitude longer than usual inter-maintenance intervals proves useful. Cyber-physical systems therefore call for an integration of various models and analysis techniques we have investigated in the past, as these cover relevant, yet hitherto isolated aspects of the dynamics exhibited by cyber-physical systems.
The tutorial will explain emerging cyber-physical systems in domains ranging from transportation to supplies, identify their requirements with respect to safety, security, reliability, and the interaction of the geometric perspective with these. It will then demonstrate automated analysis techniques for some of these aspects and will explore the scenarios they are able to cover as well as identify their limitations.
This tutorial surveys the main algorithms for verifying properties on Markov models, presents several of its applications, and highlights the main recent developments in probabilistic model checking.
| October 12 | |
|---|---|
| 8:30–10:15 | Tutorials (J Strother Moore): An Introduction to Using ACL2 |
| 10:15–10:45 | Coffee break |
| 10:45–12:30 | Tutorials (Martin Fränzle): Cyber-Physical Systems |
| 12:30–13:50 | Lunch break |
| 13:50–14:00 | Opening |
| 14:00–15:30 | SMT |
| Ruud Koolen, Tim Willemse and Hans Zantema. Using SMT for Solving Fragments of Parameterised Boolean Equation Systems | |
| Hernan Ponce-De-Leon, César Rodríguez, Josep Carmona, Keijo Heljanko and Stefan Haar. Unfolding-Based Process Discovery | |
| Ernst Althaus, Björn Beber, Joschka Kupilas and Christoph Scholl. Improving Interpolants for Linear Arithmetic | |
| 15:30–16:00 | Coffee break |
| 16:00–18:00 | Program verification |
| Thibaut Girka, David Mentré and Yann Régis-Gianas. A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences | |
| Constantin Enea, Mihaela Sighireanu and Zhilin Wu. On Automated Lemma Generation for Separation Logic with Inductive Definitions | |
| Martin Schaef and Ashish Tiwari. Severity Levels of Inconsistent Code | |
| Martin Chapman, Hana Chockler, Pascal Kesseli, Daniel Kroening, Ofer Strichman and Michael Tautschnig. Learning the Language of Error | |
| 18:30– | Reception |
| October 13 | |
| 8:30–9:30 | Invited talk (J Strother Moore): Machines Reasoning about Machines: 2015 |
| 9:30–10:00 | Coffee break |
| 10:00–12:00 | Probabilistic systems |
| Arnd Hartmanns and Holger Hermanns. Explicit Model Checking of Very Large MDP using Partitioning and Secondary Storage | |
| Yue Ben and A. Prasad Sistla. Model Checking Failure Prone Open Systems Using Probabilistic Automata | |
| Yuliya Butkova, Hassan Hatefi, Holger Hermanns and Jan Krcal. Optimal Continuous Time Markov Decisions | |
| Rachel Faran and Orna Kupferman. Spanning the Spectrum from Safety to Liveness | |
| 12:00–13:30 | Lunch break |
| 13:30–15:30 | Tool session |
| Noe Hernandez, Kerstin Eder, Evgeni Magid, Jesus Savage and David Rosenblueth. Marimba: A Tool for Verifying Properties of Hidden Markov Models | |
| Yongjian Li, Jun Pang, Yi Lv, Dongrui Fan, Shen Cao and Kaiqiang Duan. paraVerifier: An Automatic Framework for Proving Parameterized Cache Coherence Protocols | |
| Andrzej Mizera, Jun Pang and Qixia Yuan. ASSA-PBN: An Approximate Steady-state Analyser of Probabilistic Boolean Networks | |
| Mohamed Nassim Seghir and David Aspinall. EviCheck: Digital Evidence for Android | |
| Vladimir Herdt, Hoang M. Le, Daniel Grosse and Rolf Drechsler. Lazy-CSeq-SP: Boosting Sequentialization-based Verification of Multi-Threaded C Programs via Symbolic Pruning of Redundant Schedules | |
| Andrzej Murawski, Steven Ramsay and Nikos Tzevelekos. A Contextual Equivalence Checker for IMJ* | |
| 15:30– | Excursion and dinner |
| October 14 | |
| 8:30–9:30 | Invited talk (Dino Distefano): Moving fast with software verification |
| 9:30–10:00 | Coffee break |
| 10:00–12:00 | Testcase and counterexample generation |
| Thomas Ferrere, Oded Maler and Dejan Nickovic. Trace Diagnostics using Temporal Implicants | |
| Puri Arenas, Elvira Albert and Miguel Gomez-Zamalloa. Test Case Generation of Actor Systems | |
| Rachel Tzoref-Brill and Shahar Maoz. Lattice-Based Semantics for Combinatorial Model Evolution | |
| Madhavan Mukund, Gautham Shenoy R and S P Suresh. Effective verification of Replicated Data Types using Later Appearance Records (LAR) | |
| 12:00–13:30 | Lunch break |
| 13:30–15:30 | Verification |
| Chao Wang, Yi Lv and Peng Wu. TSO-to-TSO Linearizability is Undecidable | |
| Simon Bliudze, Alessandro Cimatti, Mohamad Jaber, Sergio Mover, Marco Roveri, Wajeb Saab and Wang Qiang. Formal Verification of Infinite-sate BIP models | |
| Habib Saissi, Peter Bokor and Neeraj Suri. PBMC: Symbolic Slicing for the Verification of Concurrent Programs | |
| Steen Vester. On the Complexity of Model-checking Branching and Alternating-time Temporal Logics in One-counter systems | |
| 15:30–16:00 | Coffee break |
| 16:00–18:00 | Synthesis |
| Dietmar Berwanger, Anup Basil Mathew and Marie Van Den Bogaard. Hierarchical Information Patterns and Distributed Strategy Synthesis | |
| Roderick Bloem, Rüdiger Ehlers and Robert Koenighofer. Cooperative Reactive Synthesis | |
| Andrzej Murawski, Steven Ramsay and Nikos Tzevelekos. Game Semantic Analysis of Equivalence in IMJ | |
| Paul Hunter, Guillermo Perez and Jean-Francois Raskin. Looking at Mean-Payoff through Foggy Windows | |
| October 15 | |
| 8:30–9:30 | Invited talk (Joost-Pieter Katoen): Probabilistic Programming: A True Verification Challenge |
| 9:30–10:00 | Coffee break |
| 10:00–12:00 | Hybrid systems |
| Chuchu Fan and Sayan Mitra. Bounded Verification with On-the-Fly Discrepancy Computation | |
| Liang Zou, Naijun Zhan, Shuling Wang and Martin Fränzle. Formal Verification of Simulink/Stateflow Diagrams | |
| Ting Gan, Mingshuai Chen, Liyun Dai, Bican Xia and Naijun Zhan. Decidability of the Reachability for a Family of Linear Vector Fields | |
| Jyotirmoy Deshmukh, Xiaoqing Jin, James Kapinski and Oded Maler. Stochastic Local Search for Falsification of Hybrid Systems | |
| 12:00–13:30 | Lunch break |
| 13:30–15:15 | Tutorials (Joost-Pieter Katoen): A Gentle Tutorial on Probabilistic Model Checking |