title: Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study

authors:
Håkan L. S. Younes
Marta Z. Kwiatkowska
Gethin Norman
David Parker


venue: tacas

title: Simulation-Based Iteration of Tree Transducers

authors:
Parosh Aziz Abdulla
Axel Legay
Julien d'Orso
Ahmed Rezine


title: On-the-Fly Reachability and Cycle Detection for Recursive State Machines

authors:
Rajeev Alur
Swarat Chaudhuri
Kousha Etessami
P. Madhusudan


title: Time-Efficient Model Checking with Magnetic Disk

authors:
Tonglaga Bao
Michael D. Jones


title: BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking

authors:
Damien Bergamini
Nicolas Descoubes
Christophe Joubert
Radu Mateescu


title: Empirically Efficient Verification for a Class of Infinite-State Systems

authors:
Jesse D. Bingham
Alan J. Hu


title: Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking

authors:
Ahmed Bouajjani
Peter Habermehl
Pierre Moro
Tomás Vojnar


title: JML-Testing-Tools: A Symbolic Animator for JML Specifications Using CLP

authors:
Fabrice Bouquet
Frédéric Dadeau
Bruno Legeard
Mark Utting


title: An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic

authors:
Marco Bozzano
Roberto Bruttomesso
Alessandro Cimatti
Tommi A. Junttila
Peter van Rossum
Stephan Schulz
Roberto Sebastiani


title: Java-MOP: A Monitoring Oriented Programming Environment for Java

authors:
Feng Chen
Grigore Rosu


title: SATABS: SAT-Based Predicate Abstraction for ANSI-C

authors:
Edmund M. Clarke
Daniel Kroening
Natasha Sharygina
Karen Yorav


title: Dynamic Symmetry Reduction

authors:
E. Allen Emerson
Thomas Wahl


title: Algorithmic Verification of Recursive Probabilistic State Machines

authors:
Kousha Etessami
Mihalis Yannakakis


title: DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems

authors:
Malay K. Ganai
Aarti Gupta
Pranav Ashar


title: Compositional Message Sequence Charts (CMSCs) Are Better to Implement Than MSCs


title: Snapshot Verification

authors:
Blaise Genest
Dietrich Kuske
Anca Muscholl
Doron A. Peled


title: Monte Carlo Model Checking

authors:
Radu Grosu
Scott A. Smolka


title: Truly On-the-Fly LTL Model Checking

authors:
Moritz Hammer
Alexander Knapp
Stephan Merz

abstract: We propose a novel algorithm for automata-based LTL model checking that interleaves the construction of the generalized Buchi automaton for the negation of the formula and the emptiness check. Our algorithm first converts the LTL formula into a linear weak alternating automaton; configurations of the alternating automaton correspond to the locations of a generalized Buchi automaton, and a variant of Tarjan's algorithm is used to decide the existence of an accepting run of the product of the transition system and the automaton. Because we avoid an explicit construction of the Buchi automaton, our approach can yield significant improvements in runtime and memory, for large LTL formulas. The algorithm has been implemented within the Spin model checker, and we present experimental results for some benchmark examples.


title: A New Algorithm for Strategy Synthesis in LTL Games

authors:
Aidan Harding
Mark Ryan
Pierre-Yves Schobbens


title: A Generic Theorem Prover of CSP Refinement

authors:
Yoshinao Isobe
Markus Roggenbach


title: Localization and Register Sharing for Predicate Abstraction

authors:
Himanshu Jain
Franjo Ivancic
Aarti Gupta
Malay K. Ganai


title: Symbolic Test Selection Based on Approximate Analysis

authors:
Bertrand Jeannet
Thierry Jéron
Vlad Rusu
Elena Zinovieva


title: On Some Transformation Invariants Under Retiming and Resynthesis


title: Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit

authors:
HoonSang Jin
HyoJung Han
Fabio Somenzi


title: FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs

authors:
Curtis W. Keller
Diptikalyan Saha
Samik Basu
Scott A. Smolka


title: Dependent Types for Program Understanding

authors:
Raghavan Komondoor
Ganesan Ramalingam
Satish Chandra
John Field


title: Temporal Logic for Scenario-Based Specifications

authors:
Hillel Kugler
David Harel
Amir Pnueli
Yuan Lu
Yves Bontemps


title: Complementation Constructions for Nondeterministic Automata on Infinite Words

authors:
Orna Kupferman
Moshe Y. Vardi


title: A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover

authors:
K. Rustan M. Leino
Madan Musuvathi
Xinming Ou


title: jETI: A Tool for Remote Tool Integration

authors:
Tiziana Margaria
Ralf Nagel
Bernhard Steffen


title: Using BDDs to Decide CTL


title: Applications of Craig Interpolants in Model Checking


title: Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems

authors:
Amir Pnueli
Andreas Podelski
Andrey Rybalchenko


title: Context-Bounded Model Checking of Concurrent Software

authors:
Shaz Qadeer
Jakob Rehof


title: An Abstract Interpretation-Based Refinement Algorithm for Strong Preservation

authors:
Francesco Ranzato
Francesco Tapparo


title: Model Checking Infinite-State Markov Chains

authors:
Anne Remke
Boudewijn R. Haverkort
Lucia Cloth


title: Shortest Counterexamples for Symbolic Model Checking of LTL with Past

authors:
Viktor Schuppan
Armin Biere


title: A Note on On-the-Fly Verification Algorithms

authors:
Stefan Schwoon
Javier Esparza


title: Bounded Validity Checking of Interval Duration Logic

authors:
Babita Sharma
Paritosh K. Pandya
Supratik Chakraborty


title: jMoped: A Java Bytecode Checker Based on Moped

authors:
Dejvuth Suwimonteerabuth
Stefan Schwoon
Javier Esparza


title: Using Language Inference to Verify Omega-Regular Properties

authors:
Abhay Vardhan
Koushik Sen
Mahesh Viswanathan
Gul Agha


title: Mining Temporal Specifications for Error Detection

authors:
Westley Weimer
George C. Necula


title: Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution

authors:
Tao Xie
Darko Marinov
Wolfram Schulte
David Notkin


title: MSCan - A Tool for Analyzing MSC Specifications

authors:
Benedikt Bollig
Carsten Kern
Markus Schlütter
Volker Stolz


title: Easy Parameterized Verification of Biphase Mark and 8N1 Protocols

authors:
Geoffrey M. Brown
Lee Pike


title: SAT-Based Software Certification


title: Verifying Concurrent Message-Passing C Programs with Recursive Calls

authors:
Sagar Chaki
Edmund M. Clarke
Nicholas Kidd
Thomas W. Reps
Tayssir Touili


title: Finitary Winning in omega-Regular Games

authors:
Krishnendu Chatterjee
Thomas A. Henzinger


title: Exploration of the Capabilities of Constraint Programming for Software Verification

authors:
Hélène Collavizza
Michel Rueher


title: Automatic Verification of Parameterized Data Structures

authors:
Jyotirmoy V. Deshmukh
E. Allen Emerson
Prateek Gupta


title: A Local Shape Analysis Based on Separation Logic

authors:
Dino Distefano
Peter W. O'Hearn
Hongseok Yang


title: Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs

authors:
Matthew B. Dwyer
John Hatcliff
Matthew Hoosier
Venkatesh Prasad Ranganath
Robby
Todd Wallentine


title: Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems

authors:
Javier Esparza
Stefan Kiefer
Stefan Schwoon


title: Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants

authors:
Pascal Fontaine
Jean-Yves Marion
Stephan Merz
Leonor Prensa Nieto
Alwen Fernanto Tiu


title: SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver

authors:
Malay K. Ganai
Muralidhar Talupur
Aarti Gupta


title: DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation

authors:
Hubert Garavel
Radu Mateescu
Damien Bergamini
Adrian Curic
Nicolas Descoubes
Christophe Joubert
Irina Smarandache-Sturm
Gilles Stragier


title: Compositional Model Extraction for Higher-Order Concurrent Programs

authors:
Dan R. Ghica
Andrzej S. Murawski


title: Exploiting Traces in Program Analysis

authors:
Alex Groce
Rajeev Joshi


title: Counterexample Driven Refinement for Abstract Interpretation

authors:
Bhargav S. Gulavani
Sriram K. Rajamani


title: An Experimental Comparison of the Effectiveness of Control Flow Based Testing Approaches on Seeded Faults

authors:
Atul Gupta
Pankaj Jalote


title: Why Waste a Perfectly Good Abstraction?

authors:
Arie Gurfinkel
Marsha Chechik


title: Automata-Based Verification of Programs with Tree Updates

authors:
Peter Habermehl
Radu Iosif
Tomás Vojnar


title: PRISM: A Tool for Automatic Verification of Probabilistic Systems

authors:
Andrew Hinton
Marta Z. Kwiatkowska
Gethin Norman
David Parker


title: Weighted Pushdown Systems and Trust-Management Systems

authors:
Somesh Jha
Stefan Schwoon
Hao Wang
Thomas W. Reps


title: A Practical and Complete Approach to Predicate Refinement

authors:
Ranjit Jhala
Kenneth L. McMillan


title: Widening ROBDDs with Prime Implicants

authors:
Neil Kettle
Andy King
Tadeusz Strzemecki


title: Counterexample-Guided Abstraction Refinement for the Analysis of Graph Transformation Systems

authors:
Barbara König
Vitali Kozioura


title: Approximating Predicate Images for Bit-Vector Logic

authors:
Daniel Kroening
Natasha Sharygina


title: A Region Graph Based Approach to Termination Proofs

authors:
Stefan Leue
Wei Wei


title: Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking

authors:
Bing Li
Fabio Somenzi


title: MCMAS: A Model Checker for Multi-agent Systems

authors:
Alessio Lomuscio
Franco Raimondi


title: Efficient Model Checking for LTL with Partial Order Snapshots

authors:
Peter Niebert
Doron A. Peled


title: Safety Metric Temporal Logic Is Fully Decidable

authors:
Joël Ouaknine
James Worrell


title: Model-Checking Markov Chains in the Presence of Uncertainties

authors:
Koushik Sen
Mahesh Viswanathan
Gul Agha


title: New Metrics for Static Variable Ordering in Decision Diagrams

authors:
Radu Siminiceanu
Gianfranco Ciardo


title: Simulation-Based Graph Similarity

authors:
Oleg Sokolsky
Sampath Kannan
Insup Lee


title: Efficient Guided Symbolic Reachability Using Reachability Expressions

authors:
Dina Thomas
Supratik Chakraborty
Paritosh K. Pandya


title: Parameterized Verification of pi-Calculus Systems

authors:
Ping Yang
Samik Basu
C. R. Ramakrishnan


title: Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)

authors:
Parosh Aziz Abdulla
Giorgio Delzanno
Noomene Ben Henda
Ahmed Rezine


title: Model Checking on Trees with Path Equivalences

authors:
Rajeev Alur
Pavol Cerný
Swarat Chaudhuri


title: Combining Abstraction Refinement and SAT-Based Model Checking

authors:
Nina Amla
Kenneth L. McMillan


title: Type-Dependence Analysis and Program Transformation for Symbolic Execution

authors:
Saswat Anand
Alessandro Orso
Mary Jean Harrold


title: JPF-SE: A Symbolic Execution Extension to Java PathFinder

authors:
Saswat Anand
Corina S. Pasareanu
Willem Visser


title: Abstraction Refinement of Linear Programs with Arrays

authors:
Alessandro Armando
Massimo Benerecetti
Jacopo Mantovani


title: Model Checking Liveness Properties of Genetic Regulatory Networks

authors:
Grégory Batt
Calin Belta
Ron Weiss


title: Distributed Analysis with mu CRL: A Compendium of Case Studies

authors:
Stefan Blom
Jens R. Calamé
Bert Lisser
Simona Orzan
Jun Pang
Jaco van de Pol
Muhammad Torabi Dashti
Anton Wijs


title: motor: The modestTool Environment

authors:
Henrik C. Bohnenkamp
Holger Hermanns
Joost-Pieter Katoen


title: Replaying Play In and Play Out: Synthesis of Design Models from Scenarios by Learning

authors:
Benedikt Bollig
Joost-Pieter Katoen
Carsten Kern
Martin Leucker


title: A Generic Framework for Reasoning About Dynamic Networks of Infinite-State Processes

authors:
Ahmed Bouajjani
Yan Jurski
Mihaela Sighireanu


title: Deciding Bit-Vector Arithmetic with Abstraction

authors:
Randal E. Bryant
Daniel Kroening
Joël Ouaknine
Sanjit A. Seshia
Ofer Strichman
Bryan A. Brady


title: Optimized L*-Based Assume-Guarantee Reasoning

authors:
Sagar Chaki
Ofer Strichman


title: Assume-Guarantee Synthesis

authors:
Krishnendu Chatterjee
Thomas A. Henzinger


title: A Reachability Predicate for Analyzing Low-Level Software

authors:
Shaunak Chatterjee
Shuvendu K. Lahiri
Shaz Qadeer
Zvonimir Rakamaric


title: Syntactic Optimizations for PSL Verification

authors:
Alessandro Cimatti
Marco Roveri
Stefano Tonetta


title: THERE AND BACK AGAIN: Lessons Learned on the Way to the Market


title: A Gröbner Basis Approach to CNF-Formulae Preprocessing

authors:
Christopher Condrat
Priyank Kalla


title: Automatic Analysis of the Security of XOR-Based Key Management Schemes

authors:
Véronique Cortier
Gavin Keighren
Graham Steel


title: From Time Petri Nets to Timed Automata: An Untimed Approach

authors:
Davide D'Aprile
Susanna Donatelli
Arnaud Sangnier
Jeremy Sproston


title: A Symbolic Algorithm for Optimal Markov Chain Lumping


title: Searching for Shapes in Cryptographic Protocols

authors:
Shaddin F. Doghmi
Joshua D. Guttman
F. Javier Thayer


title: Improved Algorithms for the Automata-Based Approach to Model-Checking

authors:
Laurent Doyen
Jean-François Raskin


title: Detecting Races in Ensembles of Message Sequence Charts

authors:
Edith Elkind
Blaise Genest
Doron A. Peled


title: Multi-objective Model Checking of Markov Decision Processes

authors:
Kousha Etessami
Marta Z. Kwiatkowska
Moshe Y. Vardi
Mihalis Yannakakis


title: Causal Dataflow Analysis for Concurrent Programs

authors:
Azadeh Farzan
P. Madhusudan


title: Deciding an Interval Logic with Accumulated Durations

authors:
Martin Fränzle
Michael R. Hansen


title: Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications

authors:
Marcelo F. Frias
Carlos López Pombo
Mariano M. Moscato


title: Refining Interface Alphabets for Compositional Verification

authors:
Mihaela Gheorghiu
Dimitra Giannakopoulou
Corina S. Pasareanu


title: MAVEN: Modular Aspect Verification

authors:
Max Goldman
Shmuel Katz


title: Counterexamples in Probabilistic Model Checking

authors:
Tingting Han
Joost-Pieter Katoen


title: Planned and Traversable Play-Out: A Flexible Method for Executing Scenario-Based Programs,

authors:
David Harel
Itai Segall


title: Unfolding Concurrent Well-Structured Transition Systems

authors:
Frédéric Herbreteau
Grégoire Sutre
The Quang Tran


title: Faster Algorithms for Finitary Games


title: VCEGAR: Verilog CounterExample Guided Abstraction Refinement

authors:
Himanshu Jain
Daniel Kroening
Natasha Sharygina
Edmund M. Clarke


title: State of the Union: Type Inference Via Craig Interpolation

authors:
Ranjit Jhala
Rupak Majumdar
Ru-Gang Xu


title: Model Checking Probabilistic Timed Automata with One or Two Clocks

authors:
Marcin Jurdzinski
François Laroussinie
Jeremy Sproston


title: Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking

authors:
Joost-Pieter Katoen
Tim Kemna
Ivan S. Zapreev
David N. Jansen


title: Combined Satisfiability Modulo Parametric Theories

authors:
Sava Krstic
Amit Goel
Jim Grundy
Cesare Tinelli


title: "Don't Care" Modeling: A Logical Framework for Developing Predictive System Models

authors:
Hillel Kugler
Amir Pnueli
Michael J. Stern
E. Jane Albert Hubbard


title: Uppaal/DMC- Abstraction-Based Heuristics for Directed Model Checking

authors:
Sebastian Kupferschmid
Klaus Dräger
Jörg Hoffmann
Bernd Finkbeiner
Henning Dierks
Andreas Podelski
Gerd Behrmann


title: Verifying Object-Oriented Software: Lessons and Challenges


title: Generating Representation Invariants of Structurally Complex Data

authors:
Muhammad Zubair Malik
Aman Pervaiz
Sarfraz Khurshid


title: Shape Analysis by Graph Decomposition

authors:
Roman Manevich
Josh Berdine
Byron Cook
G. Ramalingam
Mooly Sagiv


title: Checking Pedigree Consistency with PCS

authors:
Panagiotis Manolios
Marc Galceran Oms
Sergi Oliva Valls


title: The Heterogeneous Tool Set, Hets

authors:
Till Mossakowski
Christian Maeder
Klaus Lüttich


title: Hoare Logic for Realistically Modelled Machine Code

authors:
Magnus O. Myreen
Michael J. C. Gordon


title: On Sampling Abstraction of Continuous Time Logic with Durations

authors:
Paritosh K. Pandya
Shankara Narayanan Krishna
Kuntal Loya


title: Complexity in Simplicity: Flexible Agent-Based State Space Exploration

authors:
Jacob Illum Rasmussen
Gerd Behrmann
Kim Guldstrand Larsen


title: Property-Driven Partitioning for Abstraction Refinement

authors:
Roberto Sebastiani
Stefano Tonetta
Moshe Y. Vardi


title: Adaptor Synthesis for Real-Time Components

authors:
Massimo Tivoli
Pascal Fradet
Alain Girault
Gregor Gößler


title: Kodkod: A Relational Model Finder

authors:
Emina Torlak
Daniel Jackson


title: GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal Formulae

authors:
Yih-Kuen Tsay
Yu-Fang Chen
Ming-Hsien Tsai
Kang-Nien Wu
Wen-Chin Chan


title: PReMo : An Analyzer for P robabilistic Re cursive Mo dels

authors:
Dominik Wojtczak
Kousha Etessami


title: Bounded Reachability Checking of Asynchronous Systems Using Decision Diagrams

authors:
Andy Jinqing Yu
Gianfranco Ciardo
Gerald Lüttgen


title: Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations

authors:
Lijun Zhang
Holger Hermanns
Friedrich Eisenbrand
David N. Jansen


title: Computing Simulations over Tree Automata

authors:
Parosh Aziz Abdulla
Ahmed Bouajjani
Lukás Holík
Lisa Kaati
Tomás Vojnar


title: Formal Pervasive Verification of a Paging Mechanism

authors:
Eyad Alkassar
Norbert Schirmer
Artem Starostin


title: Demand-Driven Compositional Symbolic Execution

authors:
Saswat Anand
Patrice Godefroid
Nikolai Tillmann


title: Conditional Probabilities over Probabilistic and Nondeterministic Systems

authors:
Miguel E. Andrés
Peter van Rossum


title: On-the-Fly Techniques for Game-Based Software Model Checking

authors:
Adam Bakewell
Dan R. Ghica


title: Analyzing Stripped Device-Driver Executables

authors:
Gogul Balakrishnan
Thomas W. Reps


title: Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking

authors:
Jiri Barnat
Lubos Brim
Pavel Simecek
M. Weber


title: A SAT-Based Approach to Size Change Termination with Global Ranking Functions

authors:
Amir M. Ben-Amram
Michael Codish


title: Scoot: A Tool for the Analysis of SystemC Models

authors:
Nicolas Blanc
Daniel Kroening
Natasha Sharygina


title: RWset: Attacking Path Explosion in Constraint-Based Test Generation

authors:
Peter Boonstoppel
Cristian Cadar
Dawson R. Engler


title: SDSIrep: A Reputation System Based on SDSI

authors:
Ahmed Bouajjani
Javier Esparza
Stefan Schwoon
Dejvuth Suwimonteerabuth


title: Accelerating Interpolation-Based Model-Checking

authors:
Nicolas Caniart
Emmanuel Fleury
Jérôme Leroux
Marc Zeitoun


title: Efficient Automatic STE Refinement Using Responsibility

authors:
Hana Chockler
Orna Grumberg
Avi Yadgar


title: Efficient Interpolant Generation in Satisfiability Modulo Theories

authors:
Alessandro Cimatti
Alberto Griggio
Roberto Sebastiani


title: Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems

authors:
Edmund M. Clarke
Muralidhar Talupur
Helmut Veith


title: Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages

authors:
Azadeh Farzan
Yu-Fang Chen
Edmund M. Clarke
Yih-Kuen Tsay
Bow-Yaw Wang


title: RESY: Requirement Synthesis for Compositional Model Checking

authors:
Bernd Finkbeiner
Hans-Jörg Peter
Sven Schewe


title: On Verifying Fault Tolerance of Distributed Protocols

authors:
Dana Fisman
Orna Kupferman
Yoad Lustig


title: Automatically Refining Abstract Interpretations

authors:
Bhargav S. Gulavani
Supratik Chakraborty
Aditya V. Nori
Sriram K. Rajamani


title: On Local Reasoning in Verification

authors:
Carsten Ihlemann
Swen Jacobs
Viorica Sofronie-Stokkermans


title: Model Checking-Based Genetic Programming with an Application to Mutual Exclusion

authors:
Gal Katz
Doron A. Peled


title: Reasoning Algebraically About P-Solvable Loops

abstract: We present a method for generating polynomial invariants for a subfamily of imperative loops operating on numbers, called the P-solvable loops. The method uses algorithmic combinatorics and algebraic techniques. The approach is shown to be complete for some special cases. By completeness we mean that it generates a set of polynomial invariants from which, under additional assumptions, any polynomial invariant can be derived. These techniques are implemented in a new software package Aligator written in Mathematica and successfully tried on many programs implementing interesting algorithms working on numbers.


title: Fast Directed Model Checking Via Russian Doll Abstraction

authors:
Sebastian Kupferschmid
Jörg Hoffmann
Kim Guldstrand Larsen


title: Interprocedural Analysis of Concurrent Programs Under a Context Bound

authors:
Akash Lal
Tayssir Touili
Nicholas Kidd
Thomas W. Reps


title: On Automated Verification of Probabilistic Programs

authors:
Axel Legay
Andrzej S. Murawski
Joël Ouaknine
James Worrell


title: Trusted Source Translation of a Total Function Language

authors:
Guodong Li
Konrad Slind


title: Hardware Verification: Techniques, Methodology and Solutions


title: Quantified Invariant Generation Using an Interpolating Saturation Prover


title: Rocket-Fast Proof Checking for SMT Solvers


title: Z3: An Efficient SMT Solver

authors:
Leonardo Mendonça de Moura
Nikolaj S. Bjørner


title: The Real-Time Maude Tool

authors:
Peter Csaba Ölveczky
José Meseguer


title: Computation and Visualisation of Phase Portraits for Model Checking SPDIs

authors:
Gordon J. Pace
Gerardo Schneider


title: Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols

authors:
Mayank Saksena
Oskar Wibling
Bengt Jonsson


title: Symbolic Model Checking of Hybrid Systems Using Template Polyhedra

authors:
Sriram Sankaranarayanan
Thao Dang
Franjo Ivancic


title: Context-Bounded Analysis of Concurrent Queue Systems

authors:
Salvatore La Torre
P. Madhusudan
Gennaro Parlato


title: GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic

authors:
Yih-Kuen Tsay
Yu-Fang Chen
Ming-Hsien Tsai
Wen-Chin Chan
Chi-Jian Luo


title: SVISS: Symbolic Verification of Symmetric Systems

authors:
Thomas Wahl
Nicolas Blanc
E. Allen Emerson


title: Peephole Partial Order Reduction

authors:
Chao Wang
Zijiang Yang
Vineet Kahlon
Aarti Gupta


title: Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking

authors:
Martin De Wulf
Laurent Doyen
Nicolas Maquet
Jean-François Raskin


title: Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads

authors:
Mohamed Faouzi Atig
Ahmed Bouajjani
Shaz Qadeer


title: Compositional Predicate Abstraction from Game Semantics

authors:
Adam Bakewell
Dan R. Ghica


title: Alpaga: A Tool for Solving Parity Games with Imperfect Information

authors:
Dietmar Berwanger
Krishnendu Chatterjee
Martin De Wulf
Laurent Doyen
Thomas A. Henzinger

abstract: Alpaga is a solver for two-player parity games with imperfect information. Given the description of a game, it determines whether the first player can ensure to win and, if so, it constructs a winning strategy. The tool provides a symbolic implementation of a recent algorithm based on antichains.


title: Path Feasibility Analysis for String-Manipulating Programs

authors:
Nikolaj S. Bjørner
Nikolai Tillmann
Andrei Voronkov


title: Iterating Octagons

authors:
Marius Bozga
Codruta Gîrlea
Radu Iosif


title: MoonWalker: Verification of .NET Programs

authors:
Niels H. M. Aan de Brugh
Viet Yen Nguyen
Theo C. Ruys


title: Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays

authors:
Robert Brummayer
Armin Biere


title: Learning Minimal Separating DFA's for Compositional Verification

authors:
Yu-Fang Chen
Azadeh Farzan
Edmund M. Clarke
Yih-Kuen Tsay
Bow-Yaw Wang


title: Parametric Trace Slicing and Monitoring

authors:
Feng Chen
Grigore Rosu


title: Verifying Reference Counting Implementations

authors:
Michael Emmi
Ranjit Jhala
Eddie Kohler
Rupak Majumdar


title: The Complexity of Predicting Atomicity Violations

authors:
Azadeh Farzan
P. Madhusudan


title: Büchi Complementation and Size-Change Termination

authors:
Seth Fogarty
Moshe Y. Vardi


title: Ground Interpolation for the Theory of Equality

authors:
Alexander Fuchs
Amit Goel
Jim Grundy
Sava Krstic
Cesare Tinelli

abstract: Given a theory $\mathcal{T}$ and two formulas A and B jointly unsatisfiable in $\mathcal{T}$, a theory interpolant of A and B is a formula I such that (i) its non-theory symbols are shared by A and B , (ii) it is entailed by A in $\mathcal{T}$, and (iii) it is unsatisfiable with B in $\mathcal{T}$. Theory interpolants are used in model checking to accelerate the computation of reachability relations. We present a novel method for computing ground interpolants for ground formulas in the theory of equality. Our algorithm computes interpolants from colored congruence graphs representing derivations in the theory of equality. These graphs can be produced by conventional congruence closure algorithms in a straightforward manner. By working with graphs, rather than at the level of individual proof steps, we are able to derive interpolants that are pleasingly simple (conjunctions of Horn clauses) and smaller than those generated by other tools.


title: RBAC-PAT: A Policy Analysis Tool for Role Based Access Control

authors:
Mikhail I. Gofman
Ruiqi Luo
Ayla C. Solomon
Yingbin Zhang
Ping Yang
Scott D. Stoller


title: Specification Mining with Few False Positives

authors:
Claire Le Goues
Westley Weimer


title: From Tests to Proofs

authors:
Ashutosh Gupta
Rupak Majumdar
Andrey Rybalchenko


title: Semantic Reduction of Thread Interleavings in Concurrent Programs

authors:
Vineet Kahlon
Sriram Sankaranarayanan
Aarti Gupta


title: Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications

authors:
Hillel Kugler
Itai Segall


title: Computing Weakest Strategies for Safety Games of Imperfect Information

authors:
Wouter Kuijper
Jaco van de Pol


title: TaPAS: The Talence Presburger Arithmetic Suite

authors:
Jérôme Leroux
Gérald Point


title: Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches

authors:
Didier Lime
Olivier H. Roux
Charlotte Seidner
Louis-Marie Traonouez


title: All-Termination(T)

authors:
Panagiotis Manolios
Aaron Turon


title: Hierarchical Adaptive State Space Caching Based on Level Sampling

authors:
Radu Mateescu
Anton Wijs


title: Bridging the Gap Between Model-Based Development and Model Checking


title: ITPN-PerfBound: A Performance Bound Tool for Interval Time Petri Nets

authors:
Elina Pacini Naumovich
Simona Bernardi
Marco Gribaudo


title: Memoised Garbage Collection for Software Model Checking

authors:
Viet Yen Nguyen
Theo C. Ruys


title: Satisfiability Procedures for Combination of Theories Sharing Integer Offsets

authors:
Enrica Nicolini
Christophe Ringeissen
Michaël Rusinowitch


title: The YogiProject: Software Property Checking via Static Analysis and Testing

authors:
Aditya V. Nori
Sriram K. Rajamani
SaiDeep Tetali
Aditya V. Thakur


title: Static Analysis Techniques for Parameterised Boolean Equation Systems

authors:
Simona Orzan
Wieger Wesselink
Tim A. C. Willemse


title: Falsification of LTL Safety Properties in Hybrid Systems

authors:
Erion Plaku
Lydia E. Kavraki
Moshe Y. Vardi


title: Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints

authors:
Christoph Scholl
Stefan Disch
Florian Pigorsch
Stefan Kupferschmid


title: Hierarchical Set Decision Diagrams and Regular Models

authors:
Yann Thierry-Mieg
Denis Poitrenaud
Alexandre Hamez
Fabrice Kordon


title: Test Input Generation for Programs with Pointers

authors:
Dries Vanoverberghe
Nikolai Tillmann
Frank Piessens


title: Inferring Synchronization under Limited Observability

authors:
Martin T. Vechev
Eran Yahav
Greta Yorsh


title: Transition-Based Directed Model Checking

authors:
Martin Wehrle
Sebastian Kupferschmid
Andreas Podelski


title: Symbolic String Verification: Combining String Analysis and Size Analysis

authors:
Fang Yu
Tevfik Bultan
Oscar H. Ibarra


title: When Simulation Meets Antichains

authors:
Parosh Aziz Abdulla
Yu-Fang Chen
Lukás Holík
Richard Mayr
Tomás Vojnar


title: Automated Termination Analysis for Programs with Second-Order Recursion


title: Computing the Leakage of Information-Hiding Systems

authors:
Miguel E. Andrés
Catuscia Palamidessi
Peter van Rossum
Geoffrey Smith


title: ACS: Automatic Converter Synthesis for SoC Bus Protocols

authors:
Karin Avnit
Arcot Sowmya
Jorgen Peddersen


title: Preemption Sealing for Efficient Concurrency Testing

authors:
Thomas Ball
Sebastian Burckhardt
Katherine E. Coons
Madanlal Musuvathi
Shaz Qadeer


title: An Alternative to SAT-Based Approaches for Bit-Vectors

authors:
Sébastien Bardin
Philippe Herrmann
Florian Perroud


title: Boom: Taking Boolean Program Model Checking One Step Further

authors:
Gérard Basler
Matthew Hague
Daniel Kroening
C.-H. Luke Ong
Thomas Wahl
Haoxian Zhao


title: On Weak Modal Compatibility, Refinement, and the MIO Workbench

authors:
Sebastian S. Bauer
Philip Mayer
Andreas Schroeder
Rolf Hennicker


title: JTorX: A Tool for On-Line Model-Driven Test Derivation and Execution


title: The OpenSMT Solver

authors:
Roberto Bruttomesso
Edgar Pek
Natasha Sharygina
Aliaksei Tsitovich


title: AlPiNA: An Algebraic Petri Net Analyzer

authors:
Didier Buchs
Steve Hostettler
Alexis Marechal
Matteo Risoldi

abstract: AlPiNA is a graphical editor and model checker for a class of high-level Petri nets called Algebraic Petri Nets. Its main purpose is to perform reachability checks on complex models. It performs symbolic model checking based on ΣDD, an efficient evolution in the Decision Diagrams field, using novel techniques such as algebraic clustering and algebraic unfolding. AlPiNA offers a user-friendly interface, and is easily extensible.


title: Statistical Measurement of Information Leakage

authors:
Konstantinos Chatzikokolakis
Tom Chothia
Apratim Guha


title: Satisfiability Modulo the Theory of Costs: Foundations and Applications

authors:
Alessandro Cimatti
Anders Franzén
Alberto Griggio
Roberto Sebastiani
Cristian Stenico


title: Ranking Function Synthesis for Bit-Vector Relations

authors:
Byron Cook
Daniel Kroening
Philipp Rümmer
Christoph M. Wintersteiger


title: Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors

authors:
Alastair F. Donaldson
Daniel Kroening
Philipp Rümmer


title: Antichain Algorithms for Finite Automata

authors:
Laurent Doyen
Jean-François Raskin

abstract: We present a general theory that exploits simulation relations on transition systems to obtain antichain algorithms for solving the reachability and repeated reachability problems. Antichains are more succinct than the sets of states manipulated by the traditional fixpoint algorithms. The theory justifies the correctness of the antichain algorithms, and applications such as the universality problem for finite automata illustrate efficiency improvements. Finally, we show that new and provably better antichain algorithms can be obtained for the emptiness problem of alternating automata over finite and infinite words.


title: SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems

authors:
Klaus Dräger
Andrey Kupriyanov
Bernd Finkbeiner
Heike Wehrheim


title: Simplifying Linearizability Proofs with Reduction and Abstraction

authors:
Tayfun Elmas
Shaz Qadeer
Ali Sezgin
Omer Subasi
Serdar Tasiran


title: Rational Synthesis

authors:
Dana Fisman
Orna Kupferman
Yoad Lustig

abstract:
Synthesis is the automated construction of a system from its specification. The system has to satisfy its specification in all possible environments. Modern systems often interact with other systems, or agents. Many times these agents have objectives of their own, other than to fail the system. Thus, it makes sense to model system environments not as hostile, but as composed of rational agents; i.e., agents that act to achieve their own objectives.

We introduce the problem of synthesis in the context of rational agents (rational synthesis, for short). The input consists of a temporal-logic formula specifying the system, temporal-logic formulas specifying the objectives of the agents, and a solution concept definition. The output is an implementation T of the system and a profile of strategies, suggesting a behavior for each of the agents. The output should satisfy two conditions. First, the composition of T with the strategy profile should satisfy the specification. Second, the strategy profile should be an equilibrium in the sense that, in view of their objectives, agents have no incentive to deviate from the strategies assigned to them, where “no incentive to deviate” is interpreted as dictated by the given solution concept. We provide a method for solving the rational-synthesis problem, and show that for the classical definitions of equilibria studied in game theory, rational synthesis is not harder than traditional synthesis. We also consider the multi-valued case in which the objectives of the system and the agents are still temporal logic formulas, but involve payoffs from a finite lattice.


title: Efficient Büchi Universality Checking

authors:
Seth Fogarty
Moshe Y. Vardi


title: Optimal Tableau Algorithms for Coalgebraic Logics

authors:
Rajeev Goré
Clemens Kupke
Dirk Pattinson


title: PASS: Abstraction Refinement for Infinite Probabilistic Models

authors:
Ernst Moritz Hahn
Holger Hermanns
Björn Wachter
Lijun Zhang


title: Fairness for Dynamic Control

authors:
Jochen Hoenicke
Ernst-Rüdiger Olderog
Andreas Podelski


title: Blocked Clause Elimination

authors:
Matti Järvisalo
Armin Biere
Marijn Heule


title: Code Mutation in Verification and Automatic Code Correction

authors:
Gal Katz
Doron A. Peled


title: Assume-Guarantee Verification for Probabilistic Systems

authors:
Marta Z. Kwiatkowska
Gethin Norman
David Parker
Hongyang Qu


title: Approximating the Pareto Front of Multi-criteria Optimization Problems

authors:
Julien Legriel
Colas Le Guernic
Scott Cotton
Oded Maler


title: A Polymorphic Intermediate Verification Language: Design and Logical Encoding

authors:
K. Rustan M. Leino
Philipp Rümmer


title: SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata

authors:
Janusz Malinowski
Peter Niebert


title: Arrival Curves for Real-Time Calculus: The Causality Problem and Its Solutions

authors:
Matthieu Moy
Karine Altisen


title: Efficient Detection of Errors in Java Components Using Random Environment and Restarts

authors:
Pavel Parízek
Tomas Kalibera


title: Embedded Systems Design - Scientific Challenges and Work Directions


title: Simple O(m logn) Time Markov Chain Lumping

authors:
Antti Valmari
Giuliana Franceschinis


title: Tracking Heaps That Hop with Heap-Hop

authors:
Jules Villard
Étienne Lozes
Cristiano Calcagno


title: Trace-Based Symbolic Analysis for Atomicity Violations

authors:
Chao Wang
Rhishikesh Limaye
Malay K. Ganai
Aarti Gupta


title: Stranger: An Automata-Based String Analysis Tool for PHP

authors:
Fang Yu
Muath Alkhalaf
Tevfik Bultan


title: Model Checking Interactive Markov Chains

authors:
Lijun Zhang
Martin R. Neuhäußer


title: Litmus: Running Tests against Hardware

authors:
Jade Alglave
Luc Maranget
Susmit Sarkar
Peter Sewell


title: S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems

authors:
Yashwanth Annpureddy
Che Liu
Georgios Fainekos
Sriram Sankaranarayanan


title: Efficient CTMC Model Checking of Linear Real-Time Objectives

authors:
Benoît Barbot
Taolue Chen
Tingting Han
Joost-Pieter Katoen
Alexandru Mereacre


title: Model Repair for Probabilistic Systems

authors:
Ezio Bartocci
Radu Grosu
Panagiotis Katsaros
C. R. Ramakrishnan
Scott A. Smolka


title: Off-Line Test Selection with Test Purposes for Non-deterministic Timed Automata

authors:
Nathalie Bertrand
Thierry Jéron
Amélie Stainer
Moez Krichen


title: Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models

authors:
Jacob Burnim
Koushik Sen
Christos Stergiou


title: The ACL2 Sedan Theorem Proving System

authors:
Harsh Raju Chamarthi
Peter C. Dillinger
Panagiotis Manolios
Daron Vroon


title: QUASY: Quantitative Synthesis Tool

authors:
Krishnendu Chatterjee
Thomas A. Henzinger
Barbara Jobstmann
Rohit Singh


title: GAVS+: An Open Platform for the Research of Algorithmic Game Solving

authors:
Chih-Hong Cheng
Alois C. Knoll
Michael Luttenberger
Christian Buckl


title: Boosting Lazy Abstraction for SystemC with Partial Order Reduction

authors:
Alessandro Cimatti
Iman Narasamdya
Marco Roveri


title: Optimal Base Encodings for Pseudo-Boolean Constraints

authors:
Michael Codish
Yoav Fekete
Carsten Fuhs
Peter Schneider-Kamp

abstract: This paper formalizes the optimal base problem, presents an algorithm to solve it, and describes its application to the encoding of Pseudo-Boolean constraints to SAT. We demonstrate the impact of integrating our algorithm within the Pseudo-Boolean constraint solver MiniSat+. Experimentation indicates that our algorithm scales to bases involving numbers up to 1,000,000, improving on the restriction in MiniSat+ to prime numbers up to 17. We show that, while for many examples primes up to 17 do suffice, encoding with respect to optimal bases reduces the CNF sizes and improves the subsequent SAT solving time for many examples.


title: Canonized Rewriting and Ground AC Completion Modulo Shostak Theories

authors:
Sylvain Conchon
Evelyne Contejean
Mohamed Iguernelala


title: Unbeast: Symbolic Bounded Synthesis


title: Quantitative Multi-objective Verification for Probabilistic Systems

authors:
Vojtech Forejt
Marta Z. Kwiatkowska
Gethin Norman
David Parker
Hongyang Qu


title: CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes

authors:
Hubert Garavel
Frédéric Lang
Radu Mateescu
Wendelin Serwe


title: Enforcing Structural Invariants Using Dynamic Frames

authors:
Diego Garbervetsky
Daniel Gorín
Ariel Neisen


title: Compositionality Entails Sequentializability

authors:
Pranav Garg
P. Madhusudan


title: Specification-Based Program Repair Using SAT

authors:
Divya Gopinath
Muhammad Zubair Malik
Sarfraz Khurshid


title: Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic

authors:
Alberto Griggio
Thi Thieu Hoa Le
Roberto Sebastiani


title: Invariant Generation in Vampire

authors:
Krystof Hoder
Laura Kovács
Andrei Voronkov


title: Reliable Software Development: Analysis-Aware Design


title: Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference

authors:
Yungbum Jung
Wonchan Lee
Bow-Yaw Wang
Kwangkeun Yi


title: On Probabilistic Parallel Programs with Process Creation and Synchronisation

authors:
Stefan Kiefer
Dominik Wojtczak

abstract: We initiate the study of probabilistic parallel programs with dynamic process creation and synchronisation. To this end, we introduce probabilistic split-join systems (pSJSs), a model for parallel programs, generalising both probabilistic pushdown systems (a model for sequential probabilistic procedural programs which is equivalent to recursive Markov chains) and stochastic branching processes (a classical mathematical model with applications in various areas such as biology, physics, and language processing). Our pSJS model allows for a possibly recursive spawning of parallel processes; the spawned processes can synchronise and return values. We study the basic performance measures of pSJSs, especially the distribution and expectation of space, work and time. Our results extend and improve previously known results on the subsumed models. We also show how to do performance analysis in practice, and present two case studies illustrating the modelling power of pSJSs.


title: Abstractions and Pattern Databases: The Quest for Succinctness and Accuracy

authors:
Sebastian Kupferschmid
Martin Wehrle


title: Next Generation LearnLib

authors:
Maik Merten
Bernhard Steffen
Falk Howar
Tiziana Margaria


title: Transition Invariants and Transition Predicate Abstraction for Program Termination

authors:
Andreas Podelski
Andrey Rybalchenko


title: Modelling and Verification of Web Services Business Activity Protocol

authors:
Anders P. Ravn
Jirí Srba
Muhammad Saleem Vighio


title: GameTime: A Toolkit for Timing Analysis of Software

authors:
Sanjit A. Seshia
Jonathan Kotker


title: Biased Model Checking Using Flows

authors:
Muralidhar Talupur
Hyojung Han


title: Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems

authors:
Tino Teige
Martin Fränzle


title: Confluence Reduction for Probabilistic Systems

authors:
Mark Timmer
Mariëlle Stoelinga
Jaco van de Pol


title: Büchi Store: An Open Repository of Büchi Automata

authors:
Yih-Kuen Tsay
Ming-Hsien Tsai
Jinn-Shu Chang
Yi-Wen Chang


title: Loop Summarization and Termination Analysis

authors:
Aliaksei Tsitovich
Natasha Sharygina
Christoph M. Wintersteiger
Daniel Kroening


title: Applying CEGAR to the Petri Net State Equation

authors:
Harro Wimmel
Karsten Wolf


title: Counter-Example Guided Fence Insertion under TSO

authors:
Parosh Aziz Abdulla
Mohamed Faouzi Atig
Yu-Fang Chen
Carl Leonardsson
Ahmed Rezine


title: From Under-Approximations to Over-Approximations and Back

authors:
Aws Albarghouthi
Arie Gurfinkel
Marsha Chechik


title: The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures

authors:
Alessandro Armando
Wihem Arsac
Tigran Avanesov
Michele Barletta
Alberto Calvi
Alessandro Cappai
Roberto Carbone
Yannick Chevalier
Luca Compagna
Jorge Cuéllar
Gabriel Erzse
Simone Frau
Marius Minea
Sebastian Mödersheim
David von Oheimb
Giancarlo Pellegrino
Serena Elisa Ponta
Marco Rocchetto
Michaël Rusinowitch
Mohammad Torabi Dashti
Mathieu Turuani
Luca Viganò


title: LTL to Büchi Automata Translation: Fast and More Deterministic

authors:
Tomás Babiak
Mojmír Kretínský
Vojtech Rehák
Jan Strejcek

abstract: We introduce improvements in the algorithm by Gastin and Oddoux translating LTL formulae into Buchi automata via very weak alternating co-Buchi automata and generalized Buchi automata. Several improvements are based on specific properties of any formula where each branch of its syntax tree contains at least one eventually operator and at least one always operator. These changes usually result in faster translations and smaller automata. Other improvements reduce non-determinism in the produced automata. In fact, we modified all the steps of the original algorithm and its implementation known as LTL2BA. Experimental results show that our modifications are real improvements. Their implementations within an LTL2BA translation made LTL2BA very competitive with the current version of SPOT, sometimes outperforming it substantially.


title: Coupling and Importance Sampling for Statistical Model Checking

authors:
Benoît Barbot
Serge Haddad
Claudine Picaronny


title: satabs: A Bit-Precise Verifier for C Programs - (Competition Contribution)

authors:
Gérard Basler
Alastair F. Donaldson
Alexander Kaiser
Daniel Kroening
Michael Tautschnig
Thomas Wahl


title: Competition on Software Verification - (SV-COMP)


title: Bounded Phase Analysis of Message-Passing Programs

authors:
Ahmed Bouajjani
Michael Emmi


title: Deciding Conditional Termination

authors:
Marius Bozga
Radu Iosif
Filip Konecný


title: SLMC: A Tool for Model Checking Concurrent Systems against Dynamical Spatial Logic Specifications

authors:
Luís Caires
Hugo Torres Vieira


title: Reachability under Contextual Locking

authors:
Rohit Chadha
P. Madhusudan
Mahesh Viswanathan


title: Automatic Verification of Competitive Stochastic Systems

authors:
Taolue Chen
Vojtech Forejt
Marta Z. Kwiatkowska
David Parker
Aistis Simaitis


title: Context-Bounded Model Checking with ESBMC 1.17 - (Competition Contribution)

authors:
Lucas C. Cordeiro
Jeremy Morse
Denis A. Nicole
Bernd Fischer


title: A Bit Too Precise? Bounded Verification of Quantized Digital Filters

authors:
Arlen Cox
Sriram Sankaranarayanan
Bor-Yuh Evan Chang


title: Numeric Bounds Analysis with Conflict-Driven Learning

authors:
Vijay Victor D'Silva
Leopold Haller
Daniel Kroening
Michael Tautschnig


title: TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets

authors:
Alexandre David
Lasse Jacobsen
Morten Jacobsen
Kenneth Yrke Jørgensen
Mikael H. Møller
Jirí Srba


title: Predator: A Verification Tool for Programs with Dynamic Linked Data Structures - (Competition Contribution)

authors:
Kamil Dudka
Petr Müller
Petr Peringer
Tomás Vojnar


title: Automated Analysis of AODV Using UPPAAL

authors:
Ansgar Fehnker
Rob J. van Glabbeek
Peter Höfner
Annabelle McIver
Marius Portmann
Wee Lum Tan

abstract:
This paper describes an automated, formal and rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol, a popular protocol used in wireless mesh networks.

We give a brief overview of a model of AODV implemented in the UPPAAL model checker. It is derived from a process-algebraic model which reflects precisely the intention of AODV and accurately captures the protocol specification. Furthermore, we describe experiments carried out to explore AODV's behaviour in all network topologies up to 5 nodes. We were able to automatically locate problematic and undesirable behaviours. This is in particular useful to discover protocol limitations and to develop improved variants. This use of model checking as a diagnostic tool complements other formal-methods-based protocol modelling and verification techniques, such as process algebra.


title: Template-Based Controller Synthesis for Timed Systems

authors:
Bernd Finkbeiner
Hans-Jörg Peter


title: Ramsey-Based Analysis of Parity Automata

authors:
Oliver Friedmann
Martin Lange


title: HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution)

authors:
Sergey Grebenshchikov
Ashutosh Gupta
Nuno P. Lopes
Corneliu Popeea
Andrey Rybalchenko


title: Aspect-Oriented Runtime Monitor Certification

authors:
Kevin W. Hamlen
Micah Jones
Meera Sridhar


title: The Guardol Language and Verification System

authors:
David S. Hardin
Konrad Slind
Michael W. Whalen
Tuan-Hung Pham


title: Quantitative Models for a Not So Dumb Grid


title: McScM: A General Framework for the Verification of Communicating Machines

authors:
Alexander Heußner
Tristan Le Gall
Grégoire Sutre


title: Proving Reachability Using FShell - (Competition Contribution)

authors:
Andreas Holzer
Daniel Kroening
Christian Schallhart
Michael Tautschnig
Helmut Veith


title: Verifying pCTL Model Checking

authors:
Johannes Hölzl
Tobias Nipkow


title: Parameterized Synthesis

authors:
Swen Jacobs
Roderick Bloem


title: A Platform for High Performance Statistical Model Checking - PLASMA

authors:
Cyrille Jégourel
Axel Legay
Sean Sedwards


title: Modeling and Verification of a Dual Chamber Implantable Pacemaker

authors:
Zhihao Jiang
Miroslav Pajic
Salar Moarref
Rajeev Alur
Rahul Mangharam


title: Java Memory Model-Aware Model Checking

authors:
Huafeng Jin
Tuba Yavuz-Kahveci
Beverly A. Sanders


title: Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems

authors:
Frédéric Lang
Radu Mateescu


title: VATA: A Library for Efficient Manipulation of Non-deterministic Tree Automata

authors:
Ondrej Lengál
Jirí Simácek
Tomás Vojnar


title: CPAchecker with Adjustable Predicate Analysis - (Competition Contribution)

authors:
Stefan Löwe
Philipp Wendler


title: Demonstrating Learning of Register Automata

authors:
Maik Merten
Falk Howar
Bernhard Steffen
Sofia Cassel
Bengt Jonsson


title: Compositional Termination Proofs for Multi-threaded Programs

authors:
Corneliu Popeea
Andrey Rybalchenko


title: Predicate Analysis with BLAST 2.7 - (Competition Contribution)

authors:
Pavel Shved
Mikhail U. Mandrykin
Vadim S. Mutilin


title: LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation - (Competition Contribution)

authors:
Carsten Sinz
Florian Merz
Stephan Falke


title: Pushdown Model Checking for Malware Detection

authors:
Fu Song
Tayssir Touili


title: Zeno: An Automated Prover for Properties of Recursive Data Structures

authors:
William Sonnex
Sophia Drossopoulou
Susan Eisenbach


title: A Proof Assistant for Alloy Specifications

authors:
Mattias Ulbrich
Ulrich Geilmann
Aboubakr Achraf El Ghazi
Mana Taghdiri


title: Symbolic Automata: The Toolkit

authors:
Margus Veanes
Nikolaj S. Bjørner


title: Reduction-Based Formal Analysis of BGP Instances

authors:
Anduo Wang
Carolyn L. Talcott
Alexander J. T. Gurney
Boon Thau Loo
Andre Scedrov


title: Wolverine: Battling Bugs with Interpolants - (Competition Contribution)

authors:
Georg Weissenbacher
Daniel Kroening
Sharad Malik


title: Minimal Critical Subsystems for Discrete-Time Markov Models

authors:
Ralf Wimmer
Nils Jansen
Erika Ábrahám
Bernd Becker
Joost-Pieter Katoen


title: Block Abstraction Memoization for CPAchecker - (Competition Contribution)


title: QuteRTL: Towards an Open Source Framework for RTL Design Synthesis and Verification

authors:
Hu-Hsi Yeh
Cheng-Yin Wu
Chung-Yang (Ric) Huang


title: History-Aware Data Structure Repair Using SAT

authors:
Razieh Nokhbeh Zaeem
Divya Gopinath
Sarfraz Khurshid
Kathryn S. McKinley


title: CSeq: A Sequentialization Tool for C - (Competition Contribution)

authors:
Bernd Fischer
Omar Inverso
Gennaro Parlato


title: Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO

authors:
Parosh Aziz Abdulla
Mohamed Faouzi Atig
Yu-Fang Chen
Carl Leonardsson
Ahmed Rezine


title: An Integrated Specification and Verification Technique for Highly Concurrent Data Structures

authors:
Parosh Aziz Abdulla
Frédéric Haziza
Lukás Holík
Bengt Jonsson
Ahmed Rezine


title: UFO: Verification with Interpolants and Abstract Interpretation - (Competition Contribution)

authors:
Aws Albarghouthi
Arie Gurfinkel
Yi Li
Sagar Chaki
Marsha Chechik


title: Equivalence Checking of Quantum Protocols

authors:
Ebrahim Ardeshir-Larijani
Simon J. Gay
Rajagopal Nagarajan


title: On-the-Fly Exact Computation of Bisimilarity Distances

authors:
Giorgio Bacci
Giovanni Bacci
Kim G. Larsen
Radu Mardare


title: AppGuard - Enforcing User Requirements on Android Apps

authors:
Michael Backes
Sebastian Gerling
Christian Hammer
Matteo Maffei
Philipp von Styp-Rekowsky


title: Polyglot: Systematic Analysis for Multiple Statechart Formalisms

authors:
Daniel Balasubramanian
Corina S. Pasareanu
Gabor Karsai
Michael R. Lowry


title: Structural Counter Abstraction

authors:
Kshitij Bansal
Eric Koskinen
Thomas Wies
Damien Zufferey


title: Formula Preprocessing in MUS Extraction

authors:
Anton Belov
Matti Järvisalo
João Marques-Silva


title: LTL Model Checking of Interval Markov Chains

authors:
Michael Benedikt
Rastislav Lenhardt
James Worrell


title: Second Competition on Software Verification - (Summary of SV-COMP 2013)


title: Deriving Probability Density Functions from Probabilistic Functional Programs

authors:
Sooraj Bhat
Johannes Borgström
Andrew D. Gordon
Claudio V. Russo


title: Encoding Monomorphic and Polymorphic Types

authors:
Jasmin Christian Blanchette
Sascha Böhme
Andrei Popescu
Nicholas Smallbone


title: Synthesis from LTL Specifications with Mean-Payoff Objectives

authors:
Aaron Bohy
Véronique Bruyère
Emmanuel Filiot
Jean-François Raskin

abstract: The classical LTL synthesis problem is purely qualitative: the given LTL specification is realized or not by a reactive system. LTL is not expressive enough to formalize the correctness of reactive systems with respect to some quantitative aspects. This paper extends the qualitativeLTL synthesis setting to a quantitative setting. The alphabet of actions is extended with a weight function ranging over the integer numbers. The value of an infinite word is the mean-payoff of the weights of its letters. The synthesis problem then amounts to automatically construct (if possible) a reactive system whose executions all satisfy a given LTL formula and have mean-payoff values greater than or equal to some given threshold. The latter problem is called LTL$_\textsf{MP}$ synthesis and the LTL$_\textsf{MP}$ realizability problem asks to check whether such a system exists. By reduction to two-player mean-payoff parity games, we first show that LTL$_\textsf{MP}$ realizability is not more difficult than LTL realizability: it is 2ExpTime-Complete. While infinite memory strategies are required to realize LTL$_\textsf{MP}$ specifications in general, we show that e-optimality can be obtained with finite-memory strategies, for any e>0. To obtain efficient algorithms in practice, we define a Safraless procedure to decide whether there exists a finite-memory strategy that realizes a given specification for some given threshold. This procedure is based on a reduction to two-player energy safety games which are in turn reduced to safety games. Finally, we show that those safety games can be solved efficiently by exploiting the structure of their state spaces and by using antichains as a symbolic data-structure. All our results extend to multi-dimensional weights. We have implemented an antichain-based procedure and we report on some promising experimental results.


title: PRISM-games: A Model Checker for Stochastic Multi-Player Games

authors:
Taolue Chen
Vojtech Forejt
Marta Z. Kwiatkowska
David Parker
Aistis Simaitis


title: BULL: A Library for Learning Algorithms of Boolean Functions

authors:
Yu-Fang Chen
Bow-Yaw Wang


title: Proof Tree Preserving Interpolation

authors:
Jürgen Christ
Jochen Hoenicke
Alexander Nutz

abstract: Craig interpolation in SMT is difficult because, e. g., theory combination and integer cuts introduce mixed literals, i. e., literals containing local symbols from both input formulae. In this paper, we present a scheme to compute Craig interpolants in the presence of mixed literals. Contrary to existing approaches, this scheme neither limits the inferences done by the SMT solver, nor does it transform the proof tree before extracting interpolants. Our scheme works for the combination of uninterpreted functions and linear arithmetic but is extendable to other theories. The scheme is implemented in the interpolating SMT solver SMTInterpol.


title: The MathSAT5 SMT Solver

authors:
Alessandro Cimatti
Alberto Griggio
Bastiaan Joost Schaafsma
Roberto Sebastiani


title: Ramsey vs. Lexicographic Termination Proving

authors:
Byron Cook
Abigail See
Florian Zuleger


title: An Overview of the mCRL2 Toolset and Its Recent Advances

authors:
Sjoerd Cranen
Jan Friso Groote
Jeroen J. A. Keiren
Frank P. M. Stappers
Erik P. de Vink
Wieger Wesselink
Tim A. C. Willemse


title: Predator: A Tool for Verification of Low-Level List Manipulation - (Competition Contribution)

authors:
Kamil Dudka
Petr Müller
Petr Peringer
Tomás Vojnar


title: The Quest for Minimal Quotients for Probabilistic Automata

authors:
Christian Eisentraut
Holger Hermanns
Johann Schuster
Andrea Turrini
Lijun Zhang


title: LLBMC: Improved Bounded Model Checking of C Programs Using LLVM - (Competition Contribution)

authors:
Stephan Falke
Florian Merz
Carsten Sinz


title: eVolCheck: Incremental Upgrade Checker for C

authors:
Grigory Fedyukovich
Ondrej Sery
Natasha Sharygina


title: Policy Analysis for Self-administrated Role-Based Access Control

authors:
Anna Lisa Ferrara
P. Madhusudan
Gennaro Parlato


title: Unbounded Model-Checking with Interpolation for Regular Language Constraints

authors:
Graeme Gange
Jorge A. Navas
Peter J. Stuckey
Harald Søndergaard
Peter Schachte


title: Underapproximation of Procedure Summaries for Integer Programs

authors:
Pierre Ganty
Radu Iosif
Filip Konecný


title: Model Checking Database Applications

authors:
Milos Gligoric
Rupak Majumdar


title: Analysis of Boolean Programs

authors:
Patrice Godefroid
Mihalis Yannakakis


title: Runtime Verification Based on Register Automata

authors:
Radu Grigore
Dino Distefano
Rasmus Lerchedahl Petersen
Nikos Tzevelekos

abstract: We propose TOPL automata as a new method for runtime verification of systems with unbounded resource generation. Paradigmatic such systems are object-oriented programs which can dynamically generate an unbounded number of fresh object identities during their execution. Our formalism is based on register automata, a particularly successful approach in automata over infinite alphabets which administers a finite-state machine with boundedly many input-storing registers. We show that TOPL automata are equally expressive to register automata and yet suitable to express properties of programs. Compared to other runtime verification methods, our technique can handle a class of properties beyond the reach of current tools. We show in particular that properties which require value updates are not expressible with current techniques yet are naturally captured by TOPL machines. On the practical side, we present a tool for runtime verification of Java programs via TOPL properties, where the trade-off between the coverage and the overhead of the monitoring system is tunable by means of a number of parameters. We validate our technique by checking properties involving multiple objects and chaining of values on large open source projects.


title: Ultimate Automizer with SMTInterpol - (Competition Contribution)

authors:
Matthias Heizmann
Jürgen Christ
Daniel Dietsch
Evren Ermis
Jochen Hoenicke
Markus Lindenmann
Alexander Nutz
Christian Schilling
Andreas Podelski


title: Model-Checking Iterated Games

authors:
Chung-Hao Huang
Sven Schewe
Farn Wang


title: Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors

authors:
Ajith K. John
Supratik Chakraborty


title: Integer Parameter Synthesis for Timed Automata

authors:
Aleksandra Jovanovic
Didier Lime
Olivier H. Roux


title: As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty

authors:
Jean-Francois Kempf
Marius Bozga
Oded Maler


title: Model Checking Agent Knowledge in Dynamic Access Control Policies

authors:
Masoud Koleini
Eike Ritter
Mark Ryan


title: Synthesis of Circular Compositional Program Proofs via Abduction

authors:
Boyang Li
Isil Dillig
Thomas Dillig
Kenneth L. McMillan
Mooly Sagiv


title: A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems

authors:
Alexander Linden
Pierre Wolper


title: CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation - (Competition Contribution)


title: PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus

authors:
Radu Mateescu
Gwen Salaün


title: Weighted Pushdown Systems with Indexed Weight Domains


title: Handling Unbounded Loops with ESBMC 1.20 - (Competition Contribution)

authors:
Jeremy Morse
Lucas C. Cordeiro
Denis A. Nicole
Bernd Fischer


title: Automatic Testing of Real-Time Graphics Systems

authors:
Robert Nagy
Gerardo Schneider
Aram Timofeitchik


title: Threader: A Verifier for Multi-threaded Programs - (Competition Contribution)

authors:
Corneliu Popeea
Andrey Rybalchenko


title: Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking

authors:
Etienne Renault
Alexandre Duret-Lutz
Fabrice Kordon
Denis Poitrenaud


title: Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution - (Competition Contribution)

authors:
Jiri Slaby
Jan Strejcek
Marek Trtík


title: LTL Model-Checking for Malware Detection

authors:
Fu Song
Tayssir Touili


title: Intertwined Forward-Backward Reachability Analysis Using Interpolants

authors:
Yakir Vizel
Orna Grumberg
Sharon Shoham


title: CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis - (Competition Contribution)


title: Identifying Dynamic Data Structures by Learning Evolving Patterns in Memory

authors:
David H. White
Gerald Lüttgen


title: Asynchronous Multi-core Incremental SAT Solving

authors:
Siert Wieringa
Keijo Heljanko


title: Efficient Property Preservation Checking of Model Refinements

authors:
Anton Wijs
Luc Engelen


title: Forward Reachability Computation for Autonomous Max-Plus-Linear Systems

authors:
Dieky Adzkiya
Bart De Schutter
Alessandro Abate


title: SACO: Static Analyzer for Concurrent Objects

authors:
Elvira Albert
Puri Arenas
Antonio Flores-Montoya
Samir Genaim
Miguel Gómez-Zamalloa
Enrique Martin-Martin
German Puebla
Guillermo Román-Díez


title: Decision Procedures for Flat Array Properties

authors:
Francesco Alberti
Silvio Ghilardi
Natasha Sharygina


title: Discounting in LTL

authors:
Shaull Almagor
Udi Boker
Orna Kupferman

abstract: In recent years, there is growing need and interest in formalizing and reasoning about the quality of software and hardware systems. As opposed to traditional verification, where one handles the question of whether a system satisfies, or not, a given specification, reasoning about quality addresses the question of how well the system satisfies the specification. One direction in this effort is to refine the “eventually” operators of temporal logic to discounting operators: the satisfaction value of a specification is a value in [0,1], where the longer it takes to fulfill eventuality requirements, the smaller the satisfaction value is.


title: VeriMAP: A Tool for Verifying Programs through Transformations

authors:
Emanuele De Angelis
Fabio Fioravanti
Alberto Pettorossi
Maurizio Proietti


title: Verification of Concurrent Quantum Protocols by Equivalence Checking

authors:
Ebrahim Ardeshir-Larijani
Simon J. Gay
Rajagopal Nagarajan


title: SATMC: A SAT-Based Model Checker for Security-Critical Systems

authors:
Alessandro Armando
Roberto Carbone
Luca Compagna


title: Compositional Invariant Generation for Timed Systems

authors:
Lacramioara Astefanoaei
Souha Ben Rayana
Saddek Bensalem
Marius Bozga
Jacques Combaz


title: Computing Conditional Probabilities in Markovian Models Efficiently

authors:
Christel Baier
Joachim Klein
Sascha Klüppelholz
Steffen Märcker


title: CIF 3: Model-Based Engineering of Supervisory Controllers

authors:
D. A. van Beek
Wan J. Fokkink
Dennis Hendriks
Albert T. Hofkamp
Jasen Markovski
Joanna M. van de Mortel-Fronczak
Michel A. Reniers


title: Status Report on Software Verification - (Competition Summary SV-COMP 2014)


title: On the Correctness of a Branch Displacement Algorithm

authors:
Jaap Boender
Claudio Sacerdoti Coen

abstract: The branch displacement problem is a well-known problem in assembler design. It revolves around the feature, present in several processor families, of having different instructions, of different sizes, for jumps of different displacements. The problem, which is provably NP-hard, is then to select the instructions such that one ends up with the smallest possible program.


title: Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic

authors:
Marco Bozzano
Alessandro Cimatti
Marco Gario
Stefano Tonetta


title: Alternating Runtime and Size Complexity Analysis of Integer Programs

authors:
Marc Brockschmidt
Fabian Emmes
Stephan Falke
Carsten Fuhs
Jürgen Giesl


title: EDD: A Declarative Debugger for Sequential Erlang Programs

authors:
Rafael Caballero
Enrique Martin-Martin
Adrián Riesco
Salvador Tamarit


title: Proving Nontermination via Safety

authors:
Hong Yi Chen
Byron Cook
Carsten Fuhs
Kaustubh Nimkar
Peter W. O'Hearn


title: APTE: An Algorithm for Proving Trace Equivalence


title: IC3 Modulo Theories via Implicit Predicate Abstraction

authors:
Alessandro Cimatti
Alberto Griggio
Sergio Mover
Stefano Tonetta

abstract: We present a novel approach for generalizing the IC3 algorithm for invariant checking from finite-state to infinite-state transition systems, expressed over some background theories. The procedure is based on a tight integration of IC3 with Implicit (predicate) Abstraction, a technique that expresses abstract transitions without computing explicitly the abstract system and is incremental with respect to the addition of predicates. In this scenario, IC3 operates only at the Boolean level of the abstract state space, discovering inductive clauses over the abstraction predicates. Theory reasoning is confined within the underlying SMT solver, and applied transparently when performing satisfiability checks. When the current abstraction allows for a spurious counterexample, it is refined by discovering and adding a sufficient set of new predicates. Importantly, this can be done in a completely incremental manner, without discarding the clauses found in the previous search.


title: Monitoring Modulo Theories

authors:
Normann Decker
Martin Leucker
Daniel Thoma


title: Permissive Controller Synthesis for Probabilistic Systems

authors:
Klaus Dräger
Vojtech Forejt
Marta Z. Kwiatkowska
David Parker
Mateusz Ujma


title: Predator: A Shape Analyzer Based on Symbolic Memory Graphs - (Competition Contribution)

authors:
Kamil Dudka
Petr Peringer
Tomás Vojnar


title: SMT-Based Verification of Software Countermeasures against Side-Channel Attacks

authors:
Hassan Eldib
Chao Wang
Patrick Schaumont


title: Ultimate Kojak - (Competition Contribution)

authors:
Evren Ermis
Alexander Nutz
Daniel Dietsch
Jochen Hoenicke
Andreas Podelski


title: Analyzing the Next Generation Airborne Collision Avoidance System

authors:
Christian von Essen
Dimitra Giannakopoulou


title: Detecting Unrealizable Specifications of Distributed Systems

authors:
Bernd Finkbeiner
Leander Tentrup


title: Characterizing Algebraic Invariants by Differential Radical Invariants

authors:
Khalil Ghorbal
André Platzer


title: FDR3 - A Modern Refinement Checker for CSP

authors:
Thomas Gibson-Robinson
Philip J. Armstrong
Alexandre Boulgakov
A. W. Roscoe


title: FrankenBit: Bit-Precise Verification with Many Bits - (Competition Contribution)

authors:
Arie Gurfinkel
Anton Belov


title: Synthesizing Safe Bit-Precise Invariants

authors:
Arie Gurfinkel
Anton Belov
João Marques-Silva


title: The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification

authors:
Arnd Hartmanns
Holger Hermanns


title: Ultimate Automizer with Unsatisfiable Cores - (Competition Contribution)

authors:
Matthias Heizmann
Jürgen Christ
Daniel Dietsch
Jochen Hoenicke
Markus Lindenmann
Betim Musa
Christian Schilling
Stefan Wissert
Andreas Podelski


title: Quasi-Equal Clock Reduction: More Networks, More Queries

authors:
Christian Herrera
Bernd Westphal
Andreas Podelski


title: Symbolic Synthesis for Epistemic Specifications with Observational Semantics

authors:
Xiaowei Huang
Ron van der Meyden


title: PEALT: An Automated Reasoning Tool for Numerical Aggregation of Trust Evidence

authors:
Michael Huth
Jim Huan-Pu Kuo


title: Lazy-CSeq: A Lazy Sequentialization Tool for C - (Competition Contribution)

authors:
Omar Inverso
Ermenegildo Tomasco
Bernd Fischer
Salvatore La Torre
Gennaro Parlato


title: Environment-Model Based Testing of Control Systems: Case Studies

authors:
Erwan Jahier
Simplice Djoko Djoko
Chaouki Maiza
Eric Lafont


title: CBMC - C Bounded Model Checker - (Competition Contribution)

authors:
Daniel Kroening
Michael Tautschnig


title: Variations on Safety


title: Ranking Templates for Linear Loops

authors:
Jan Leike
Matthias Heizmann


title: Synthesis for Human-in-the-Loop Control Systems

authors:
Wenchao Li
Dorsa Sadigh
S. Shankar Sastry
Sanjit A. Seshia


title: Concurrent Depth-First Search Algorithms

abstract: We present concurrent algorithms, based on depth-first search, for three problems relevant to model checking: given a state graph, to find its strongly connected components, which states are in loops, and which states are in “lassos”. Our algorithms typically exhibit about a four-fold speed-up over the corresponding sequential algorithms on an eight-core machine. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


title: CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses - (Competition Contribution)

authors:
Stefan Löwe
Mikhail U. Mandrykin
Philipp Wendler


title: Learning Regular Languages over Large Alphabets

authors:
Oded Maler
Irini-Eleftheria Mens

abstract: Apprentissage de langages réguliers sur des alphabets de grandes tailles L'apprentissage de langages réguliers est un sous-ensemble de l'apprentissage automatique qui s'est révélé utile dans de nombreux domaines tels que l'intelli-gence artificielle, les réseaux de neurones, l'exploration de données, la vérification, etc. De plus, l'intérêt dans les langages définis sur des alphabets infinis ou de grande taille est croissant au fil des années. Même si plusierurs propriétés et théories se généralisent à partir du cas fini, l'apprentissage de tels langages est une tâche difficile.En effet, dans ce contexte, l'application naïve des algorithmes d'apprentissage traditionnel n'est pas possible.Dans cette thèse, nous présentons un schéma algorithmique général pour l'ap-prentissage de langages définis sur des alphabets infinis ou de grande taille, comme par exemple des sous-ensembles bornés de N or R ou des vecteurs booléens de grandes dimensions. Nous nous restreignons aux classes de langages qui sont acceptés par des automates déterministes symboliques utilisant des prédicats pour définir les transitions, construisant ainsi une partition finie de l'alphabet pour chaque état.Notre algorithme d'apprentissage, qui est une adaptation du L* d'Angluin, combine l'apprentissage classique d'un automate par la caractérisation de ses états, avec l'apprentissage de prédicats statiques définissant les partitions de l'alphabet. Nous utilisons l'apprentissage incrémental avec la propriété que deux types de requêtes fournissent une information suffisante sur le langage cible. Les requêtes du premier type sont les requêtes d'adhésions, qui permettent de savoir si un mot proposé appartient ou non au langage cible. Les requêtes du second type sont les requêtes d'équivalence, qui vérifient si un automate proposé accepte le langage cible; dans le cas contraire, un contre-exemple est renvoyé.Nous étudions l'apprentissage de langages définis sur des alphabets infinis ou de grande tailles dans un cadre théorique et général, mais notre objectif est de proposer des solutions concrètes pour un certain nombre de cas particuliers. Ensuite, nous nous intéressons aux deux principaux aspects du problème. Dans un premier temps, nous supposerons que les requêtes d'équivalence renvoient toujours un contre-exemple minimal pour un ordre de longueur-lexicographique quand l'automate proposé est incorrect. Puis dans un second temps, nous relâchons cette hypothèse forte d'un oracle d'équivalence, et nous la remplaçons avec une hypothèse plus réaliste où l'équivalence est approchée par un test sur les requêtes qui utilisent un échantillonnage sur l'ensemble des mots. Dans ce dernier cas, ce type de requêtes ne garantit pas l'obtention de contre-exemples, et par conséquent de contre-exemples minimaux. Nous obtenons alors une notion plus faible d'apprent-issage PAC (Probably Approximately Correct), permettant l'apprentissage d'une approximation du langage cible.Tout les algorithmes ont été implémentés, et leurs performances, en terme de construction d'automate et de taille d'alphabet, ont été évaluées empiriquement.


title: ESBMC 1.22 - (Competition Contribution)

authors:
Jeremy Morse
Mikhail Ramalho
Lucas C. Cordeiro
Denis A. Nicole
Bernd Fischer


title: CPAlien: Shape Analyzer for CPAChecker - (Competition Contribution)

authors:
Petr Müller
Tomás Vojnar


title: GRASShopper - Complete Heap Verification with Mixed Specifications

authors:
Ruzica Piskac
Thomas Wies
Damien Zufferey


title: Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems

authors:
Thomas Reinbacher
Kristin Yvonne Rozier
Johann Schumann


title: Basic Problems in Multi-View Modeling

authors:
Jan Reineke
Stavros Tripakis


title: Symbolic Model Checking of Stutter-Invariant Properties Using Generalized Testing Automata

authors:
Ala-Eddine Ben Salem
Alexandre Duret-Lutz
Fabrice Kordon
Yann Thierry-Mieg


title: Bounds2: A Tool for Compositional Multi-parametrised Verification


title: Symbiotic 2: More Precise Slicing - (Competition Contribution)

authors:
Jiri Slaby
Jan Strejcek


title: Precise Approximations of the Probability Distribution of a Markov Process in Time: An Application to Probabilistic Invariance

authors:
Sadegh Esmaeil Zadeh Soudjani
Alessandro Abate


title: MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings - (Competition Contribution)

authors:
Ermenegildo Tomasco
Omar Inverso
Bernd Fischer
Salvatore La Torre
Gennaro Parlato


title: Are Timed Automata Bad for a Specification Language? Language Inclusion Checking for Timed Automata

authors:
Ting Wang
Jun Sun
Yang Liu
Xinyu Wang
Shanping Li


title: GPUexplore: Many-Core On-the-Fly State Space Exploration Using GPUs

authors:
Anton Wijs
Dragan Bosnacki


title: Software Verification and Verifiable Witnesses - (Report on SV-COMP 2015)


title: Stateless Model Checking for TSO and PSO

authors:
Parosh Aziz Abdulla
Stavros Aronis
Mohamed Faouzi Atig
Bengt Jonsson
Carl Leonardsson
Konstantinos Sagonas


title: Non-cumulative Resource Analysis

authors:
Elvira Albert
Jesús Correas Fernández
Guillermo Román-Díez


title: FramewORk for Embedded System verification - (Competition Contribution)

authors:
Pablo González de Aledo
Pablo Sánchez Espeso


title: Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis

authors:
Rajeev Alur
Salar Moarref
Ufuk Topcu


title: SAM: The Static Analysis Module of the MAVERIC Mobile App Security Verification Platform

authors:
Alessandro Armando
Gianluca Bocci
Giantonio Chiarelli
Gabriele Costa
Gabriele De Maglie
Rocco Mammoliti
Alessio Merlo


title: Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives

authors:
Nicolas Basset
Marta Z. Kwiatkowska
Ufuk Topcu
Clemens Wiltsche


title: νZ - An Optimizing SMT Solver

authors:
Nikolaj S. Bjørner
Anh-Dung Phan
Lars Fleckenstein


title: Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information

authors:
Roderick Bloem
Krishnendu Chatterjee
Swen Jacobs
Robert Könighofer

abstract: Synthesis of program parts is particularly useful for concurrent systems. However, most approaches do not support common design tasks, like modifying a single process without having to re-synthesize or verify the whole system. Assume-guarantee synthesis AGS provides robustness against modifications of system parts, but thus far has been limited to the perfect information setting. This means that local variables cannot be hidden from other processes, which renders synthesis results cumbersome or even impossible to realize. We resolve this shortcoming by defining AGS under partial information. We analyze the complexity and decidability in different settings, showing that the problem has a high worst-case complexity and is undecidable in many interesting cases. Based on these observations, we present a pragmatic algorithm based on bounded synthesis, and demonstrate its practical applicability on several examples.


title: Shield Synthesis: - Runtime Enforcement for Reactive Systems

authors:
Roderick Bloem
Bettina Könighofer
Robert Könighofer
Chao Wang

abstract: Scalability issues may prevent users from verifying critical properties of a complex hardware design. In this situation, we propose to synthesize a "safety shield" that is attached to the design to enforce the properties at run time. Shield synthesis can succeed where model checking and reactive synthesis fail, because it only considers a small set of critical properties, as opposed to the complex design, or the complete specification in the case of reactive synthesis. The shield continuously monitors the input/output of the design and corrects its erroneous output only if necessary, and as little as possible, so other non-critical properties are likely to be retained. Although runtime enforcement has been studied in other domains such as action systems, reactive systems pose unique challenges where the shield must act without delay. We thus present the first shield synthesis solution for reactive hardware systems and report our experimental results. This is an extended version of [5], featuring an additional appendix.


title: Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving

authors:
Jeroen Bransen
L. Thomas van Binsbergen
Koen Claessen
Atze Dijkstra


title: MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives

authors:
Tomás Brázdil
Krishnendu Chatterjee
Vojtech Forejt
Antonín Kucera

abstract: We present MultiGain, a tool to synthesize strategies for Markov decision processes MDPs with multiple mean-payoff objectives. Our models are described in PRISM, and our tool uses the existing interface and simulator of PRISM. Our tool extends PRISM by adding novel algorithms for multiple mean-payoff objectives, and also provides features such as ii¾?generating strategies and exploring them for simulation, and checking them with respect to other properties; and iii¾?generating an approximate Pareto curve for two mean-payoff objectives. In addition, we present a new practical algorithm for the analysis of MDPs with multiple mean-payoff objectives under memoryless strategies.


title: Perentie: Modular Trace Refinement and Selective Value Tracking - (Competition Contribution)

authors:
Franck Cassez
Takashi Matsuoka
Edward Pierzchalski
Nathan Smyth


title: On Parallel Scalable Uniform SAT Witness Generation

authors:
Supratik Chakraborty
Daniel J. Fremont
Kuldeep S. Meel
Sanjit A. Seshia
Moshe Y. Vardi


title: Commutativity of Reducers

authors:
Yu-Fang Chen
Chih-Duo Hong
Nishant Sinha
Bow-Yaw Wang


title: CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation - (Competition Contribution)

authors:
Yu-Fang Chen
Chiao Hsieh
Ming-Hsien Tsai
Bow-Yaw Wang
Farn Wang


title: Approximate Counting in SMT and Value Estimation for Probabilistic Programs

authors:
Dmitry Chistikov
Rayna Dimitrova
Rupak Majumdar


title: HyComp: An SMT-Based Model Checker for Hybrid Systems

authors:
Alessandro Cimatti
Alberto Griggio
Sergio Mover
Stefano Tonetta


title: An LTL Proof System for Runtime Verification

authors:
Clare Cini
Adrian Francalanza


title: Fairness for Infinite-State Systems

authors:
Byron Cook
Heidy Khlaaf
Nir Piterman

abstract: In this paper we introduce the first known tool for symbolically proving fair-CTL properties of infinite-state integer programs. Our solution is based on a reduction to existing techniques for fairness-free CTL model checking via the use of infinite non-deterministic branching to symbolically partition fair from unfair executions. We show the viability of our approach in practice using examples drawn from device drivers and algorithms utilizing shared resources.


title: CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic - (Competition Contribution)

authors:
Matthias Dangl
Stefan Löwe
Philipp Wendler


title: Uppaal Stratego

authors:
Alexandre David
Peter Gjøl Jensen
Kim Guldstrand Larsen
Marius Mikucionis
Jakob Haahr Taankvist


title: syntMaskFT: A Tool for Synthesizing Masking Fault-Tolerant Programs from Deontic Specifications

authors:
Ramiro Demasi
Pablo F. Castro
Nicolás Ricci
Thomas Stephen Edward Maibaum
Nazareno Aguirre

abstract: In this paper we introduce syntMaskFT, a tool that synthesizes fault-tolerant programs from specifications written in a fragment of branching time logic with deontic operators, designed for specifying fault-tolerant systems. The tool focuses on producing masking tolerant programs, that is, programs that during a failure mask faults in such a way that they cannot be observed by the environment. It is based on an algorithm we have introduced in previous work, and shown to be sound and complete. syntMaskFT takes a specification and automatically determines whether a masking fault-tolerant component is realizable; in such a case, a description of the component is produced together with the maximal set of faults that can be supported for this level of tolerance. We present the ideas behind the tool by means of a simple example, and also report the result of experiments realized with more complex case studies.


title: Sylvan: Multi-Core Decision Diagrams

authors:
Tom van Dijk
Jaco van de Pol


title: BINSEC: Binary Code Analysis with Low-Level Regions

authors:
Adel Djoudi
Sébastien Bardin


title: C2E2: A Verification Tool for Stateflow Models

authors:
Parasara Sridhar Duggirala
Sayan Mitra
Mahesh Viswanathan
Matthew Potok


title: Nested Antichains for WS1S

authors:
Tomás Fiedor
Lukás Holík
Ondrej Lengál
Tomás Vojnar


title: Insight: An Open Binary Analysis Framework

authors:
Emmanuel Fleury
Olivier Ly
Gérald Point
Aymeric Vincent


title: Model Checking Gene Regulatory Networks

authors:
Mirco Giacobbe
Calin C. Guet
Ashutosh Gupta
Thomas A. Henzinger
Tiago Paixão
Tatjana Petrov

abstract: The behaviour of gene regulatory networks GRNs is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner's weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs -an important problem of interest in evolutionary biology- more efficiently than the classical simulation method. We specify the property in linear temporal logics. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights.


title: Scalable Timing Analysis with Refinement

authors:
Nan Guan
Yue Tang
Jakaria Abdullah
Martin Stigge
Wang Yi


title: SeaHorn: A Framework for Verifying C Programs (Competition Contribution)

authors:
Arie Gurfinkel
Temesghen Kahsai
Jorge A. Navas


title: Semantic Importance Sampling for Statistical Model Checking

authors:
Jeffery P. Hansen
Lutz Wrage
Sagar Chaki
Dionisio de Niz
Mark H. Klein


title: SMACK+Corral: A Modular Verifier - (Competition Contribution)

authors:
Arvind Haran
Montgomery Carter
Michael Emmi
Akash Lal
Shaz Qadeer
Zvonimir Rakamaric


title: Ultimate Automizer with Array Interpolation - (Competition Contribution)

authors:
Matthias Heizmann
Daniel Dietsch
Jan Leike
Betim Musa
Andreas Podelski

abstract: Ultimate Automizer is a software verification tool that is able to analyze reachability of an error label, memory safety, and termination of C programs. For all three tasks, our tool follows an automatabased approach where interpolation is used to compute proofs for traces. The interpolants are generated via a new scheme that requires only the post operator, unsatisfiable cores and live variable analysis. This new scheme enables our tool to use the SMT theory of arrays in combination with interpolation.


title: Forester: Shape Analysis Using Tree Automata - (Competition Contribution)

authors:
Lukás Holík
Martin Hruska
Ondrej Lengál
Adam Rogalewicz
Jirí Simácek
Tomás Vojnar


title: Verified Reachability Analysis of Continuous Systems


title: A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System

authors:
Jean-Baptiste Jeannin
Khalil Ghorbal
Yanni Kouskoulas
Ryan W. Gardner
Aurora C. Schmidt
Erik Zawadzki
André Platzer


title: LTSmin: High-Performance Language-Independent Model Checking

authors:
Gijs Kant
Alfons Laarman
Jeroen Meijer
Jaco van de Pol
Stefan Blom
Tom van Dijk


title: Limit Deterministic and Probabilistic Automata for LTL ∖ GU

authors:
Dileep Kini
Mahesh Viswanathan


title: dReach: δ-Reachability Analysis for Hybrid Systems

authors:
Soonho Kong
Sicun Gao
Wei Chen
Edmund M. Clarke


title: Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip

authors:
Abderahman Kriouile
Wendelin Serwe


title: Value Slice: A New Slicing Concept for Scalable Property Checking

authors:
Shrawan Kumar
Amitabha Sanyal
Uday P. Khedker


title: Saturation-Based Incremental LTL Model Checking with Inductive Proofs

authors:
Vince Molnár
Dániel Darvas
András Vörös
Tamás Bartha


title: Predator Hunting Party (Competition Contribution)

authors:
Petr Müller
Petr Peringer
Tomás Vojnar


title: Analysis of Dynamic Process Networks

authors:
Kedar S. Namjoshi
Richard J. Trefler


title: Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches - (Competition Contribution)

authors:
Truc L. Nguyen
Bernd Fischer
Salvatore La Torre
Gennaro Parlato


title: ULTIMATE KOJAK with Memory Safety Checks - (Competition Contribution)

authors:
Alexander Nutz
Daniel Dietsch
Mostafa Mahmoud Mohamed
Andreas Podelski


title: MarQ: Monitoring at Runtime with QEA

authors:
Giles Reger
Helena Cuenca Cruz
David E. Rydeheard


title: Parallel Explicit Model Checking for Generalized Büchi Automata

authors:
Etienne Renault
Alexandre Duret-Lutz
Fabrice Kordon
Denis Poitrenaud


title: Symbolic Quantitative Robustness Analysis of Timed Automata

abstract: We study the robust safety problem for timed automata under guard imprecisions which consists in computing an imprecision parameter under which a safety specification holds. We give a symbolic semi-algorithm for the problem based on a parametric data structure, and evaluate its performance in comparison with a recently published one, and with a binary search on enlargement values.


title: Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions

authors:
Roberto Sebastiani
Patrick Trentin

abstract:
In the last decade we have witnessed an impressive progress in the expressiveness and efficiency of Satisfiability Modulo Theories SMT solving techniques. This has brought previously-intractable problems at the reach of state-of-the-art SMT solvers, in particular in the domain of SW and HW verification. Many SMT-encodable problems of interest, however, require also the capability of finding models that are optimal wrt. some cost functions. In previous work, namely Optimization Modulo Theory with Linear Rational Cost Functions --- OMT $\mathcal{LRA}\cup \mathcal{T}$ , we have leveraged SMT solving to handle the minimization of cost functions on linear arithmetic over the rationals, by means of a combination of SMT and LP minimization techniques.

In this paper we push the envelope of our OMT approach along three directions: first, we extend it to work with linear arithmetic on the mixed integer/rational domain, by means of a combination of SMT, LP and ILP minimization techniques; second, we develop a multi-objective version of OMT, so that to handle many cost functions simultaneously or lexicographically; third, we develop an incremental version of OMT, so that to exploit the incrementality of some OMT-encodable problems. An empirical evaluation performed on OMT-encoded verification problems demonstrates the usefulness and efficiency of these extensions.


title: FAUST  2 : Formal Abstractions of Uncountable-STate STochastic Processes

authors:
Sadegh Esmaeil Zadeh Soudjani
Caspar Gevaerts
Alessandro Abate

abstract: FAUST $^{\mathsf 2}$ is a software tool that generates formal abstractions of possibly non-deterministic discrete-time Markov processes dtMP defined over uncountable continuous state spaces. A dtMP model is specified in MATLAB and abstracted as a finite-state Markov chain or a Markov decision process. The abstraction procedure runs in MATLAB and employs parallel computations and fast manipulations based on vector calculus, which allows scaling beyond state-of-the-art alternatives. The abstract model is formally put in relationship with the concrete dtMP via a user-defined maximum threshold on the approximation error introduced by the abstraction procedure. FAUST $^{\mathsf 2}$ allows exporting the abstract model to well-known probabilistic model checkers, such as PRISM or MRMC. Alternatively, it can handle internally the computation of PCTL properties e.g. safety or reach-avoid over the abstract model. FAUST $^{\mathsf 2}$ allows refining the outcomes of the verification procedures over the concrete dtMP in view of the quantified and tunable error, which depends on the dtMP dynamics and on the given formula. The toolbox is available at http://sourceforge.net/projects/faust2/


title: AProVE: Termination and Memory Safety of C Programs - (Competition Contribution)

authors:
Thomas Ströder
Cornelius Aschermann
Florian Frohn
Jera Hensel
Jürgen Giesl


title: Symbolic Model-Checking Using ITS-Tools


title: MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings - (Competition Contribution)

authors:
Ermenegildo Tomasco
Omar Inverso
Bernd Fischer
Salvatore La Torre
Gennaro Parlato


title: Verifying Concurrent Programs by Memory Unwinding


title: AutoProof: Auto-Active Functional Verification of Object-Oriented Programs

authors:
Julian Tschannen
Carlo A. Furia
Martin Nordio
Nadia Polikarpova


title: Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling

authors:
Hiroshi Unno
Tachio Terauchi


title: FuncTion: An Abstract Domain Functor for Termination - (Competition Contribution)


title: Cascade - (Competition Contribution)

authors:
Wei Wang
Clark W. Barrett


title: GPU Accelerated Strong and Branching Bisimilarity Checking


title: A Method for Improving the Precision and Coverage of Atomicity Violation Predictions

authors:
Reng Zeng
Zhuo Sun
Su Liu
Xudong He


title: Advances in Symbolic Probabilistic Model Checking with PRISM

authors:
Joachim Klein
Christel Baier
Philipp Chrszon
Marcus Daum
Clemens Dubslaff
Sascha Klüppelholz
Steffen Märcker
David Müller


title: Reduction of Nondeterministic Tree Automata

authors:
Ricardo Almeida
Lukás Holík
Richard Mayr

abstract:
We present an efficient algorithm to reduce the size of nondeterministic tree automata, while retaining their language. It is based on new transition pruning techniques, and quotienting of the state space w.r.t. suitable equivalences. It uses criteria based on combinations of downward and upward simulation preorder on trees, and the more general downward and upward language inclusions. Since tree-language inclusion is EXPTIME-complete, we describe methods to compute good approximations in polynomial time.

We implemented our algorithm as a module of the well-known libvata tree automata library, and tested its performance on a given collection of tree automata from various applications of libvata in regular model checking and shape analysis, as well as on various classes of randomly generated tree automata. Our algorithm yields substantially smaller and sparser automata than all previously known reduction techniques, and it is still fast enough to handle large instances.


title: Acceleration in Multi-PushDown Systems

authors:
Mohamed Faouzi Atig
K. Narayan Kumar
Prakash Saivasan


title: TcT: Tyrolean Complexity Tool

authors:
Martin Avanzini
Georg Moser
Michael Schaper


title: Finding Recurrent Sets with Backward Analysis and Trace Partitioning

authors:
Alexey Bakhirkin
Nir Piterman

abstract: We propose an abstract-interpretation-based analysis for recurrent sets. A recurrent set is a set of states from which the execution of a program cannot or might not as in our case escape. A recurrent set is a part of a program's non-termination proof that needs to be complemented by reachability analysis. We find recurrent sets by performing a potentially over-approximate backward analysis that produces an initial candidate. We then perform over-approximate forward analysis on the candidate to check and refine it and ensure soundness. In practice, the analysis relies on trace partitioning that predicts future paths through the program that non-terminating executions will take. Using our technique, we were able to find recurrent sets in many benchmarks found in the literature including some that, to our knowledge, cannot be handled by existing tools. In addition, we note that typically, analyses that search for recurrent sets are applied to linear under-approximations of programs or employ some form of non-approximate numeric reasoning. In contrast, our analysis uses standard abstract-interpretation techniques and is potentially applicable to a larger class of abstract domains and therefore --- programs.


title: Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2016)


title: The xSAP Safety Analysis Platform

authors:
Benjamin Bittner
Marco Bozzano
Roberto Cavada
Alessandro Cimatti
Marco Gario
Alberto Griggio
Cristian Mattarei
Andrea Micheli
Gianni Zampedri

abstract: This paper describes the xSAP safety analysis platform. xSAP provides several model-based safety analysis features for finite- and infinite-state synchronous transition systems. In particular, it supports library-based definition of fault modes, an automatic model extension facility, generation of safety analysis artifacts such as Dynamic Fault Trees and Failure Mode and Effects Analysis tables. Moreover, it supports probabilistic evaluation of Fault Trees, failure propagation analysis using Timed Failure Propagation Graphs, and Common Cause Analysis. xSAP has been used in several industrial projects as verification back-end, and is currently being evaluated in a joint R&D Project involving FBK and The Boeing Company.


title: Complementing Semi-deterministic Büchi Automata

authors:
Frantisek Blahoudek
Matthias Heizmann
Sven Schewe
Jan Strejcek
Ming-Hsien Tsai


title: Approaching the Coverability Problem Continuously

authors:
Michael Blondin
Alain Finkel
Christoph Haase
Serge Haddad

abstract: The coverability problem for Petri nets plays a central role in the verification of concurrent shared-memory programs. However, its high EXPSPACE-complete complexity poses a challenge when encountered in real-world instances. In this paper, we develop a new approach to this problem which is primarily based on applying forward coverability in continuous Petri nets as a pruning criterion inside a backward coverability framework. A cornerstone of our approach is the efficient encoding of a recently developed polynomial-time algorithm for reachability in continuous Petri nets into SMT. We demonstrate the effectiveness of our approach on standard benchmarks from the literature, which shows that our approach decides significantly more instances than any existing tool and is in addition often much faster, in particular on large instances.


title: Uncertainty Propagation Using Probabilistic Affine Forms and Concentration of Measure Inequalities

authors:
Olivier Bouissou
Eric Goubault
Sylvie Putot
Aleksandar Chakarov
Sriram Sankaranarayanan


title: T2: Temporal Property Verification

authors:
Marc Brockschmidt
Byron Cook
Samin Ishtiaq
Heidy Khlaaf
Nir Piterman

abstract: We present the open-source tool T2, the first public release from the TERMINATOR projecti??[9]. T2 has been extended over the past decade to support automatic temporal-logic proving techniques and to handle a general class of user-provided liveness and safety properties. Input can be provided in a native format and in C, via the support of the LLVM compiler framework. We briefly discuss T2's architecture, its underlying techniques, and conclude with an experimental illustration of its competitiveness and directions for future extensions.


title: FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals

authors:
Radu Calinescu
Kenneth Johnson
Colin Paterson


title: Efficient Syntax-Driven Lumping of Differential Equations

authors:
Luca Cardelli
Mirco Tribastone
Max Tschaikowski
Andrea Vandin

abstract: We present an algorithm to compute exact aggregations of a class of systems of ordinary differential equations ODEs. Our approach consists in an extension of Paige and Tarjan's seminal solution to the coarsest refinement problem by encoding an ODE system into a suitable discrete-state representation. In particular, we consider a simple extension of the syntax of elementary chemical reaction networks because i it can express ODEs with derivatives given by polynomials of degree at most two, which are relevant in many applications in natural sciences and engineering; and ii we can build on two recently introduced bisimulations, which yield two complementary notions of ODE lumping. Our algorithm computes the largest bisimulations in $$Or \cdot s \cdot \log s$$ time, where r is the number of monomials and s is the number of variables in the ODEs. Numerical experiments on real-world models from biochemistry, electrical engineering, and structural mechanics show that our prototype is able to handle ODEs with millions of variables and monomials, providing significant model reductions.


title: PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems

authors:
Milan Ceska
Petr Pilar
Nicola Paoletti
Lubos Brim
Marta Z. Kwiatkowska


title: Deductive Proofs of Almost Sure Persistence and Recurrence Properties

authors:
Aleksandar Chakarov
Yuen-Lam Voronin
Sriram Sankaranarayanan


title: Symbiotic 3: New Slicer and Error-Witness Generation - (Competition Contribution)

authors:
Marek Chalupa
Martin Jonás
Jiri Slaby
Jan Strejcek
Martina Vitovská


title: Parametric Runtime Verification of C Programs

authors:
Zhe Chen
Zhemin Wang
Yunlong Zhu
Hongwei Xi
Zhibin Yang

abstract: Many runtime verification tools are built based on Aspect-Oriented Programming (AOP) tools, most often AspectJ, a mature implementation of AOP for Java. Although already popular in the Java domain, there is few work on runtime verification of C programs via AOP, due to the lack of a solid language and tool support. In this paper, we propose a new general purpose and expressive language for defining monitors as an extension to the C language, and present our tool implementation of the weaver, the Movec compiler, which brings fully-fledged parametric runtime verification support into the C domain. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


title: Integrated Environment for Diagnosing Verification Errors

authors:
Maria Christakis
K. Rustan M. Leino
Peter Müller
Valentin Wüstholz


title: Cerberus: Automated Synthesis of Enforcement Mechanisms for Security-Sensitive Business Processes

authors:
Luca Compagna
Daniel Ricardo dos Santos
Serena Elisa Ponta
Silvio Ranise