ATVA 2015

13th International Symposium on Automated Technology for Verification and Analysis

October 12–15, 2015, Shanghai, China


J Strother Moore: Machines Reasoning about Machines: 2015

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.

Dino Distefano: Moving fast with software verification

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.

Joost-Pieter Katoen: Probabilistic Programming: A True Verification Challenge

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?


J Strother Moore: An Introduction to Using ACL2

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.

Martin Fränzle: Cyber-Physical Systems

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.

Joost-Pieter Katoen: A Gentle Tutorial on Probabilistic Model Checking

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