Venues / CAV /

CAV 2018

70 papers

A Counting Semantics for Monitoring LTL Specifications over Finite Traces · Ezio Bartocci, Roderick Bloem, Dejan Nickovic, Franz Röck
A Direct Encoding for NNC Polyhedra · Anna Becchi, Enea Zaffanella
ADAC: Automated Design of Approximate Circuits · Milan Ceska, Jirí Matyás, Vojtech Mrazek, Lukás Sekanina, Zdenek Vasícek, Tomás Vojnar
Android Stack Machine · Taolue Chen, Jinlong He, Fu Song, Guozhen Wang, Zhilin Wu, Jun Yan
Attracting Tangles to Solve Parity Games · Tom van Dijk
Automata vs Linear-Programming Discounted-Sum Inclusion · Suguman Bansal, Swarat Chaudhuri, Moshe Y. Vardi
Btor2 , BtorMC and Boolector 3.0 · Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere
Constrained Dynamic Partial Order Reduction · Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel, Albert Rubio
Constraint-Based Synthesis of Coupling Proofs · Aws Albarghouthi, Justin Hsu
Continuous Formal Verification of Amazon s2n · Andrey Chudnov, Nathan Collins, Byron Cook, Joey Dodds, Brian Huffman, Colm MacCárthaigh + 6 more
Controller Synthesis Made Real: Reach-Avoid Specifications and Linear Dynamics · Chuchu Fan, Umang Mathur, Sayan Mitra, Mahesh Viswanathan
Counterexample Guided Inductive Synthesis Modulo Theories · Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen
Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains · Qiyi Tang, Franck van Breugel
Delta-Decision Procedures for Exists-Forall Problems over the Reals · Soonho Kong, Armando Solar-Lezama, Sicun Gao
Eager Abstraction for Symbolic Model Checking · Kenneth L. McMillan
Exploiting Synchrony and Symmetry in Relational Verification · Lauren Pick, Grigory Fedyukovich, Aarti Gupta
Fast Numerical Program Analysis with Reinforcement Learning · Gagandeep Singh, Markus Püschel, Martin T. Vechev
Formal Reasoning About the Security of Amazon Web Services · Byron Cook
Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System · Mark Tullsen, Lee Pike, Nathan Collins, Aaron Tomb
Formally Verified Montgomery Multiplication · Christoph Walther
Foundations and Tools for the Static Analysis of Ethereum Smart Contracts · Ilya Grishchenko, Matteo Maffei, Clara Schneidewind
From Programs to Interpretable Deep Models and Back · Eran Yahav
Inner and Outer Approximating Flowpipes for Delay Differential Equations · Eric Goubault, Sylvie Putot, Lorenz Sahlmann
JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode · Lucas C. Cordeiro, Pascal Kesseli, Daniel Kroening, Peter Schrammel, Marek Trtík
Layered Concurrent Programs · Bernhard Kragl, Shaz Qadeer
Lazy Self-composition for Security Verification · Weikun Yang, Yakir Vizel, Pramod Subramanyan, Aarti Gupta, Sharad Malik
Learning Abstractions for Program Synthesis · Xinyu Wang, Greg Anderson, Isil Dillig, Kenneth L. McMillan
Let this Graph Be Your Witness! - An Attestor for Verifying Java Pointer Programs · Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll
MaxSMT-Based Type Inference for Python 3 · Mostafa Hassan, Caterina Urban, Marco Eilers, Peter Müller
Model Checking Boot Code from AWS Data Centers · Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle
Model Checking Indistinguishability of Randomized Security Protocols · Matthew S. Bauer, Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan
Model Checking Quantitative Hyperproperties · Bernd Finkbeiner, Christopher Hahn, Hazem Torfah
Model Generation for Quantified Formulas: A Taint-Based Approach · Benjamin Farinier, Sébastien Bardin, Richard Bonichon, Marie-Laure Potet
Monitoring CTMCs by Multi-clock Timed Automata · Yijun Feng, Joost-Pieter Katoen, Haokun Li, Bican Xia, Naijun Zhan
Monitoring Weak Consistency · Michael Emmi, Constantin Enea
Nagini: A Static Verifier for Python · Marco Eilers, Peter Müller
On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony · Ahmed Bouajjani, Constantin Enea, Kailiang Ji, Shaz Qadeer
Partial Order Aware Concurrency Sampling · Xinhao Yuan, Junfeng Yang, Ronghui Gu
Peregrine: A Tool for the Analysis of Population Protocols · Michael Blondin, Javier Esparza, Stefan Jaax
Permission Inference for Array Programs · Jérôme Dohrau, Alexander J. Summers, Caterina Urban, Severin Münger, Peter Müller
Program Analysis Is Harder Than Verification: A Computability Perspective · Patrick Cousot, Roberto Giacobazzi, Francesco Ranzato
Propositional Dynamic Logic for Higher-Order Functional Programs · Yuki Satake, Hiroshi Unno
Quasi-Optimal Partial Order Reduction · Huyen T. T. Nguyen, César Rodríguez, Marcelo Sousa, Camille Coti, Laure Petrucci
Rabinizer 4: From LTL to Your Favourite Deterministic Automaton · Jan Kretínský, Tobias Meggendorfer, Salomon Sickert, Christopher Ziegler
Reachable Set Over-Approximation for Nonlinear Systems Using Piecewise Barrier Tubes · Hui Kong, Ezio Bartocci, Thomas A. Henzinger
Reactive Control Improvisation · Daniel J. Fremont, Sanjit A. Seshia
Reasoning About TSO Programs Using Reduction and Abstraction · Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, Serdar Tasiran
SCInfer: Refinement-Based Verification of Software Countermeasures Against Side-Channel Attacks · Jun Zhang, Pengfei Gao, Fu Song, Chao Wang
Safety-Aware Apprenticeship Learning · Weichao Zhou, Wenchao Li
Semantic Adversarial Deep Learning · Tommaso Dreossi, Somesh Jha, Sanjit A. Seshia
SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate Reachability · Jianwen Li, Rohit Dureja, Geguang Pu, Kristin Yvonne Rozier, Moshe Y. Vardi
Solving Quantified Bit-Vectors Using Invertibility Conditions · Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Sound Value Iteration · Tim Quatmann, Joost-Pieter Katoen
Space-Time Interpolants · Goran Frehse, Mirco Giacobbe, Thomas A. Henzinger
Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems · Frederik M. Bønneland, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marco Muñiz, Jirí Srba
StringFuzz: A Fuzzer for String Solvers · Dmitry Blotsky, Federico Mora, Murphy Berzish, Yunhui Zheng, Ifaz Kabir, Vijay Ganesh
Strix: Explicit Reactive Synthesis Strikes Back! · Philipp J. Meyer, Salomon Sickert, Michael Luttenberger
Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives · Krishnendu Chatterjee, Monika Henzinger, Veronika Loitzenbauer, Simin Oraee, Viktor Toman
Symbolic Liveness Analysis of Real-World Software · Daniel Schemmel, Julian Büning, Oscar Soria Dustmann, Thomas Noll, Klaus Wehrle
Syntax-Guided Synthesis with Quantitative Syntactic Objectives · Qinheping Hu, Loris D'Antoni
Syntax-Guided Termination Analysis · Grigory Fedyukovich, Yueling Zhang, Aarti Gupta
Synthesis of Asynchronous Reactive Programs from Temporal Specifications · Suguman Bansal, Kedar S. Namjoshi, Yaniv Sa'ar
Synthesizing Reactive Systems from Hyperproperties · Bernd Finkbeiner, Christopher Hahn, Philip Lukert, Marvin Stenger, Leander Tentrup
The DEEPSEC Prover · Vincent Cheval, Steve Kremer, Itsaka Rakotonirina
The JKind Model Checker · Andrew Gacek, John Backes, Mike Whalen, Lucas G. Wagner, Elaheh Ghassabani
The Learnability of Symbolic Automata · George Argyros, Loris D'Antoni
The Proof Complexity of SMT Solvers · Robert Robere, Antonina Kolokolova, Vijay Ganesh
Understanding and Extending Incremental Determinization for 2QBF · Markus N. Rabe, Leander Tentrup, Cameron Rasmussen, Sanjit A. Seshia
Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm · Edon Kelmendi, Julia Krämer, Jan Kretínský, Maximilian Weininger
What's Hard About Boolean Functional Synthesis? · S. Akshay, Supratik Chakraborty, Shubham Goel, Sumith Kulal, Shetal Shah