Русский
English| Philipp Ruemmer, Hossein Hojjat and Viktor Kuncak | Disjunctive Interpolants for Horn-Clause Verification | |
| Oshri Adler, Cindy Eisner and Tatyana Veksler | Relative Equivalence in the Presence of Ambiguity | |
| Alberto Puggelli, Wenchao Li, Alberto Sangiovanni-Vincentelli and Sanjit Seshia | Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties | |
| Hui Kong, Fei He, Xiaoyu Song, William Hung and Ming Gu | Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems | |
| Guanfeng Lv, Kaile Su and Yanyan Xu | CacBDD: A BDD Package with Dynamic Cache Management | |
| Andrew Reynolds, Cesare Tinelli, Amit Goel and Sava Krstic | Finite Model Finding in SMT | |
| Pierre Ganty and Samir Genaim | Proving Termination Starting from the End | |
| Supratik Chakraborty, Kuldeep S. Meel and Moshe Vardi | A Scalable and Nearly Uniform Generator of SAT Witnesses | |
| Marc Brockschmidt, Byron Cook and Carsten Fuhs | Better termination proving through cooperation | |
| Chih-Hong Cheng, Harald Ruess and Natarajan Shankar | JBernstein: A Validity Checker for Generalized Polynomial Constraints | |
| Arun Chaganty, Akash Lal, Aditya Nori and Sriram Rajamani | Combining Relational Learning with SMT Solvers using CEGAR | |
| Krishnendu Chatterjee and Jakub Łącki | Faster Algorithms for Markov Decision Processes with Low Treewidth | |
| Christoph Haase, Samin Ishtiaq, Joel Ouaknine and Matthew Parkinson | SeLoger: A Tool for Graph-Based Reasoning in Separation Logic | |
| William Harris, Guoliang Jin, Shan Lu and Somesh Jha | Validating Library Usage Interactively | |
| Isil Dillig and Thomas Dillig | EXPLAIN: A Tool for Performing Abductive Inference | |
| Brad Bingham, Jesse Bingham, John Erickson and Mark Greenstreet | Distributed Explicit State Model Checking of Deadlock Freedom | |
| Pranav Garg, Christof Loding, P. Madhusudan and Daniel Neider | Learning Universally Quantified Invariants of Linear Data Structures | |
| Cezara Dragoi, Ashutosh Gupta and Thomas Henzinger | Automatic linearizability proofs of concurrent objects with cooperating updates | |
| Aleksandar Chakarov and Sriram Sankaranarayanan | Probabilistic Program Analysis with Martingales | |
| Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, Fabio Merli and Enrico Tronci | System Level Formal Verification via Model Checking Driven Simulation | |
| Romain Brenguier | PRALINE: A Tool for Computing Nash Equilibria in Concurrent Games | |
| Simon Meier, Benedikt Schmidt, Cas Cremers and David Basin | The TAMARIN Prover for the Symbolic Analysis of Security Protocols | |
| Johannes G. Reiter, Ivana Bozic, Krishnendu Chatterjee and Martin A. Nowak | TTP: Tool for Tumor Progression | |
| Adi Sosnovich, Orna Grumberg and Gabi Nakibly | Finding Security Vulnerabilities in a Network Protocol using Parameterized Systems | |
| Krishnendu Chatterjee, Andreas Gaiser and Jan Kretinsky | Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis | |
| Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki and Edmund Clarke | Automatic Abstraction in SMT-Based Unbounded Software Model Checking | |
| Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach | Efficient synthesis for concurrency using semantics-preserving transformations | |
| Jade Alglave, Daniel Kroening and Michael Tautschnig | Partial Orders for Efficient BMC of Concurrent Software | |
| Azadeh Farzan and Zachary Kincaid | Duet: Static Analysis for Unbounded Parallelism | |
| Roy Armoni, Dana Fisman and Naiyong Jin | SVA and PSL Local Variables – A Practical Approach | |
| Aws Albarghouthi and Ken Mcmillan | Beautiful Interpolants | |
| Ocan Sankur | Shrinktech: A Tool for the Robustness Analysis of Timed Automata | |
| Jiri Barnat, Lubos Brim, Vojtěch Havel, Jan Havlíček, Jan Kriho, Milan Lenco, Petr Ročkai, Vladimír Štill and Jiří Weiser | DiVinE 3.0 — Explicit-state Model-checker for Multithreaded C/C++ Programs | |
| Tom Chothia, Yusuke Kawamoto and Chris Novakovic | A Tool for Estimating Information Leakage | |
| Koen Claessen, Jasmin Fisher, Samin Ishtiaq, Nir Piterman and Qinsi Wang | Model-Checking Signal Transduction Networks through Decreasing Reachability Sets | |
| Shaull Almagor, Guy Avni and Orna Kupferman | Automatic Generation of Quality Specifications | |
| Loris D’Antoni and Margus Veanes | Equivalence of Extended Symbolic Finite Transducers | |
| Pierre Ganty, Javier Esparza and Rupak Majumdar | Parameterized Verification of Asynchronous Shared-Memory Systems | |
| Thomas Braibant and Adam Chlipala | Formal Verification of Hardware Synthesis | |
| Vincent Cheval, Veronique Cortier and Antoine Plet | Lengths may break privacy — or how to check for equivalences with length | |
| Fabrizio Biondi, Andrzej Wasowski, Axel Legay and Louis-Marie Traonouez | QUAIL: a quantitative security analyzer for imperative code | |
| Ruzica Piskac, Thomas Wies and Damien Zufferey | Automating Separation Logic using SMT | |
| Pavithra Prabhakar and Miriam Garcia Soto | Abstraction based Model-Checking of Stability of Hybrid Systems | |
| Alfons Laarman, Mads Chr. Olesen, Andreas Engelbredt Dalsgaard, Kim Guldstrand Larsen and Jaco Van De Pol | Multi-Core Emptiness Checking of Timed B\”uchi Automata using Inclusion Abstraction | |
| Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleks Nanevski and Mooly Sagiv | Effectively Propositional Reasoning about Reachability in Linked Data Structures | |
| Lubos Brim, Milan Ceska, Sven Drazan and David Šafránek | Exploring Parameter Space of Stochastic Biochemical Systems using Quantitative Model Checking | |
| Daniel Wonisch, Alexander Schremmer and Heike Wehrheim | Programs from Proofs – A PCC Alternative | |
| Richard Uhler and Nirav Dave | Seri: Automatic Translation of High-level Symbolic Computations into SMT Queries | |
| Maximilien Colange, Souheib Baarir, Fabrice Kordon and Yann Thierry-Mieg | Towards Software Model Checking using Data Decision Diagrams | |
| Cyrille Jegourel, Axel Legay and Sean Sedwards | Importance Splitting for Statistical Model Checking Rare Properties | |
| Aws Albarghouthi, Sumit Gulwani and Zachary Kincaid | Recursive Program Synthesis | |
| Daniel Kroening, Matt Lewis and Georg Weissenbacher | Under-Approximating Loops in C Programs for Fast Counterexample Detection | |
| Alexandre Donzé, Thomas Ferrere and Oded Maler | Efficient Robust Monitoring for STL | |
| Tewodros Beyene, Corneliu Popeea and Andrey Rybalchenko | Solving Existentially Quantified Horn Clauses | |
| Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf and Jan-Georg Smaus | A Fully Verified Executable LTL Model Checker | |
| Christian Von Essen and Barbara Jobstmann | Program Repair without Regret | |
| Alistair Stewart, Kousha Etessami and Mihalis Yannakakis | Upper bounds for Newton’s method on monotone polynomial systems, and P-time model checking of probabilistic one-counter automata | |
| Sudhindra Pandav, Maheshwar Singh and Hemanthkumar Sivaraj | End-to-end Runtime Validation of Intel(R) Transactional Synchronization Extensions | |
| Yakir Vizel, Vadim Ryvchin and Alexander Nadel | Efficient Generation of Small Interpolants in CNF | |
| Frédéric Herbreteau, B Srivathsan and Igor Walukiewicz | Lazy abstractions for timed automata | |
| Xin Chen, Erika Abraham and Sriram Sankaranarayanan | Flow*: An Analyzer for Non-Linear Hybrid Systems | |
| Loïc Paulevé, Geoffroy Andrieux and Heinz Koeppl | Under-approximating Cut Sets for Reachability in Large Scale Automata Networks | |
| Joao Marques-Silva, Mikolas Janota and Anton Belov | Minimal Sets over Monotone Predicates in Boolean Formulae | |
| Johannes Kloos, Rupak Majumdar, Filip Niksic and Ruzica Piskac | Incremental, Inductive Coverability | |
| Étienne André, Yang Liu, Jun Sun, Jin Song Dong and Shang-Wei Lin | PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems | |
| Panagiotis Manolios and Vasilis Papavasileiou | ILP Modulo Theories | |
| Liyun Dai, Bican Xia and Naijun Zhan | Generating Non-Linear Interpolants by Semidefinite Programming | |
| Ming-Hsien Tsai, Yih-Kuen Tsay and Yu-Shiang Hwang | GOAL for Games, Omega-Automata, and Logics | |
| Lukas Holik, Ondrej Lengal, Adam Rogalewicz, Jiri Simacek and Tomas Vojnar | Fully Automated Shape Analysis Based on Forest Automata | |
| Ayrat Khalimov, Swen Jacobs and Roderick Bloem | PARTY: Parameterized Synthesis of Token Rings |