CAV 2019: 31ST INTERNATIONAL CONFERENCE ON COMPUTER AIDED VERIFICATION

A
Albarghouthi, Aws	Efficient Synthesis with Probabilistic Constraints
André, Étienne	Symbolic Monitoring against Specifications Parametric in Time and Data
Arcaini, Paolo	Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification
Arcak, Murat	Flexible Computational Pipelines for Robust Abstraction-based Control Synthesis
Arechiga, Nikos	Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
Ashok, Pranav	PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
Avni, Guy	Run-Time Optimization for Learned Controllers through Quantitative Games
B
Backes, John	Reachability Analysis for AWS-based Networks
Bansal, Suguman	Safety and co-safety comparator automata for discounted-sum inclusion
Barbosa, Haniel	CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis
Barrett, Clark	High-Level Abstractions for Simplifying Extended String Constraints in SMT CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis The Marabou Framework for Verification and Analysis of Deep Neural Networks Invertibility Conditions for Floating-Point Formulas
Bayless, Sam	Reachability Analysis for AWS-based Networks
Becker, Heiko	Icing: Supporting Fast-math Style Optimizations in a Verified Compiler
Beckett, Ryan	Efficient verification of network fault tolerance via counterexample-guided refinement
Beillahi, Sidi Mohamed	Checking Robustness Against Snapshot Isolation
Berkovits, Idan	Verification of Threshold-based Distributed Algorithms by Decomposition to Decidable Logics
Biswas, Ranadeep	On the Complexity of Checking Consistency for Replicated Data Types
Bloem, Roderick	Run-Time Optimization for Learned Controllers through Quantitative Games
Bouajjani, Ahmed	Gradual Consistency Checking Checking Robustness Against Snapshot Isolation
Brain, Martin	Invertibility Conditions for Floating-Point Formulas
Breck, Jason	Proving Unrealizability for Syntax-Guided Synthesis
Busatto-Gaston, Damien	Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach
C
Cerny, Pavol	Quantitative Mitigation of Timing Side Channels
Ceska, Milan	Semi-Quantitative Abstraction and Analysis of Chemical Reaction Networks
Chatterjee, Krishnendu	Run-Time Optimization for Learned Controllers through Quantitative Games
Chen, Mingshuai	Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations
Cimatti, Alessandro	Extending nuXmv with Timed Transition Systems and Timed Temporal Properties
Coenen, Norine	Verifying Hyperliveness
Cook, Byron	Reachability Analysis for AWS-based Networks
Cyphert, John	Proving Unrealizability for Syntax-Guided Synthesis
D
D'Antoni, Loris	Symbolic Register Automata Efficient Synthesis with Probabilistic Constraints Proving Unrealizability for Syntax-Guided Synthesis
Damian, Andrei	Communication-closed asynchronous protocols
Darulova, Eva	Icing: Supporting Fast-math Style Optimizations in a Verified Compiler Sound Approximation of Programs with Elementary Functions
Davis, Jennifer	When Human Intuition Fails: Using Formal Methods to Find an Error in the “Proof” of a Multi-Agent Protocol
Deshmukh, Jyotirmoy	Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
Dill, David	The Marabou Framework for Verification and Analysis of Deep Neural Networks
Dimitrova, Rayna	Synthesizing Approximate Implementations for Unrealizable Specifications
Dodge, Catherine	Reachability Analysis for AWS-based Networks
Dragoi, Cezara	Communication-closed asynchronous protocols
Dreossi, Tommaso	Verifai: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems
Drews, Samuel	Efficient Synthesis with Probabilistic Constraints
E
Elfar, Mahmoud	Security-Aware Synthesis Using Delayed-Action Games
Emmi, Michael	On the Complexity of Checking Consistency for Replicated Data Types Violat: Generating Tests of Observational Refinement for Concurrent Objects
Enea, Constantin	Gradual Consistency Checking Checking Robustness Against Snapshot Isolation On the Complexity of Checking Consistency for Replicated Data Types Violat: Generating Tests of Observational Refinement for Concurrent Objects
Ernst, Gidon	SecCSL: Security Concurrent Separation Logic
Erradi, Mohammed	Gradual Consistency Checking
F
Farzan, Azadeh	Automated Hypersafety Verification
Faymonville, Peter	StreamLAB: Stream-based Monitoring of Cyber-Physical Systems
Fedyukovich, Grigory	Quantified Invariants via Syntax-Guided-Synthesis
Feldman, Yotam M. Y.	Inferring Inductive Invariants from Phase Structures
Feng, Shenghua	Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations
Ferreira, Tiago	Symbolic Register Automata
Finkbeiner, Bernd	Synthesizing Approximate Implementations for Unrealizable Specifications Temporal Stream Logic: Synthesis beyond the Bools Verifying Hyperliveness StreamLAB: Stream-based Monitoring of Cyber-Physical Systems
Frohn, Florian	Termination of Triangular Integer Loops is Decidable
Fränzle, Martin	Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations
Furbach, Florian	BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings
G
Gacek, Andrew	Reachability Analysis for AWS-based Networks
Ganesh, Vijay	Interpolating Strong Induction
Gao, Sicun	Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
García Soto, Miriam	Membership-based Synthesis of Linear Hybrid Automata
Gastin, Paul	Fast algorithms for handling diagonal constraints in timed automata
Gavrilenko, Natalia	BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings
Ghosh, Shromona	Verifai: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems
Giannarakis, Nick	Efficient verification of network fault tolerance via counterexample-guided refinement
Giesl, Jürgen	Termination of Triangular Integer Loops is Decidable
Gomes, Victor B. F.	Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C
Griggio, Alberto	Extending nuXmv with Timed Transition Systems and Timed Temporal Properties
Guo, Xiaojie	Integrating Formal Schedulability Analysis into a Verifed OS Kernel
Gupta, Aarti	Quantified Invariants via Syntax-Guided-Synthesis
Gurfinkel, Arie	Interpolating Strong Induction Property Directed Self Composition
H
Hasuo, Ichiro	Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification Symbolic Monitoring against Specifications Parametric in Time and Data
Heljanko, Keijo	BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings
Henzinger, Thomas A.	Membership-based Synthesis of Linear Hybrid Automata Run-Time Optimization for Learned Controllers through Quantitative Games
Hong, Chih-Duo	Probabilistic Bisimulation for Parameterized Systems
Hu, A.J.	Reachability Analysis for AWS-based Networks
Hu, Qinheping	Proving Unrealizability for Syntax-Guided Synthesis
Huang, Derek	The Marabou Framework for Verification and Analysis of Deep Neural Networks
Humphrey, Laura	When Human Intuition Fails: Using Formal Methods to Find an Error in the “Proof” of a Multi-Agent Protocol
Hur, Chung-Kil	AliveInLean: A Verified LLVM Peephole Optimization Verifier
I
Ibeling, Duligur	The Marabou Framework for Verification and Analysis of Deep Neural Networks
Iosif, Radu	Alternating Automata Modulo First Order Theories
J
J. Fremont, Daniel	Verifai: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems
Jagannathan, Suresh	Automated Parameterized Verification of CRDTs
Jain, Mitesh	Local and Compositional Reasoning For Optimized Reactive Systems
Jonáš, Martin	Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors
Julian, Kyle	The Marabou Framework for Verification and Analysis of Deep Neural Networks
K
Kahsai, Temesghen	Reachability Analysis for AWS-based Networks
Kang, Eunsuk	Automated Synthesis of Secure Platform Mappings
Kapinski, James	Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
Katz, Guy	The Marabou Framework for Verification and Analysis of Deep Neural Networks
Kim, Edward	Verifai: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems
Kim, Eric	Flexible Computational Pipelines for Robust Abstraction-based Control Synthesis
Kincaid, Zachary	Loop Summarization with Rational Vector Addition Systems
Kingston, Derek	When Human Intuition Fails: Using Formal Methods to Find an Error in the “Proof” of a Multi-Agent Protocol
Klein, Felix	Temporal Stream Logic: Synthesis beyond the Bools
Kochenderfer, Mykel	The Marabou Framework for Verification and Analysis of Deep Neural Networks
Kocik, Bill	Reachability Analysis for AWS-based Networks
Kong, Soonho	Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
Kotelnikov, Evgenii	Reachability Analysis for AWS-based Networks
Kretinsky, Jan	Semi-Quantitative Abstraction and Analysis of Chemical Reaction Networks PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
Kukovec, Jure	Reachability Analysis for AWS-based Networks
Kölbl, Martin	Clock Bound Repair for Timed Systems
Könighofer, Bettina	Run-Time Optimization for Learned Controllers through Quantitative Games
L
Lafortune, Stephane	Automated Synthesis of Secure Platform Mappings
Lal, Akash	Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers
Lau, Stella	Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C
Lazarus, Christopher	The Marabou Framework for Verification and Analysis of Deep Neural Networks
Lazic, Marijana	Verification of Threshold-based Distributed Algorithms by Decomposition to Decidable Logics
Lee, Juneyoung	AliveInLean: A Verified LLVM Peephole Optimization Verifier
Lesourd, Maxime	Integrating Formal Schedulability Analysis into a Verifed OS Kernel
Leue, Stefan	Clock Bound Repair for Timed Systems
Li, Jianwen	Satisfiability Checking for Mission-Time LTL
Li, Yangjia	Formal verification of quantum algorithms using quantum Hoare logic
Lim, Rachel	The Marabou Framework for Verification and Analysis of Deep Neural Networks
Lin, Anthony Widjaja	Probabilistic Bisimulation for Parameterized Systems
Liu, Junyi	Formal verification of quantum algorithms using quantum Hoare logic
Liu, Mengqi	Integrating Formal Schedulability Analysis into a Verifed OS Kernel
Liu, Peizun	Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers
Liu, Tao	Formal verification of quantum algorithms using quantum Hoare logic
Lopes, Nuno P.	AliveInLean: A Verified LLVM Peephole Optimization Verifier
Lossa, Giuliano	Verification of Threshold-based Distributed Algorithms by Decomposition to Decidable Logics
M
Madhukar, Kumar	Quantified Invariants via Syntax-Guided-Synthesis
Madsen, Curtis	STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis
Magnago, Enrico	Extending nuXmv with Timed Transition Systems and Timed Temporal Properties
Mahajan, Ratul	Efficient verification of network fault tolerance via counterexample-guided refinement
Majumdar, Rupak	Probabilistic Bisimulation for Parameterized Systems
Manolios, Panagiotis	Local and Compositional Reasoning For Optimized Reactive Systems
Markey, Nicolas	Abstraction Refinement Algorithms for Timed Automata
McLaughlin, Sean	Reachability Analysis for AWS-based Networks
Memarian, Kayvan	Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C
Meyer, Roland	BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings
Militaru, Alexandru	Communication-closed asynchronous protocols
Millstein, Todd	Overfitting in Synthesis: Theory and Practice
Monmege, Benjamin	Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach
Mukherjee, Sayan	Fast algorithms for handling diagonal constraints in timed automata
Murray, Toby	SecCSL: Security Concurrent Separation Logic
Myers, Chris J.	STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis
Myreen, Magnus O.	Icing: Supporting Fast-math Style Optimizations in a Verified Compiler
N
Nagar, Kartik	Automated Parameterized Verification of CRDTs
Neupane, Thakur	STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis
Niemetz, Aina	Invertibility Conditions for Floating-Point Formulas
Noetzli, Andres	High-Level Abstractions for Simplifying Extended String Constraints in SMT CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis
Nori, Aditya	Overfitting in Synthesis: Theory and Practice
P
Padhi, Saswat	Overfitting in Synthesis: Theory and Practice
Padon, Oded	Verification of Threshold-based Distributed Algorithms by Decomposition to Decidable Logics
Pajic, Miroslav	Security-Aware Synthesis Using Delayed-Action Games
Pichon-Pharabod, Jean	Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C
Piskac, Ruzica	Temporal Stream Logic: Synthesis beyond the Bools
Ponce-De-Leon, Hernan	BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings
Prabhu, Sumanth	Quantified Invariants via Syntax-Guided-Synthesis
Pranger, Stefan	Run-Time Optimization for Learned Controllers through Quantitative Games
Preiner, Mathias	Invertibility Conditions for Floating-Point Formulas
R
Rabe, Markus N.	Incremental Determinization for Quantifier Elimination and Functional Synthesis
Ravanbakhsh, Hadi	Verifai: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems
Reed, Jason	Reachability Analysis for AWS-based Networks
Reps, Thomas	Proving Unrealizability for Syntax-Guided Synthesis
Reynier, Pierre-Alain	Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach
Reynolds, Andrew	High-Level Abstractions for Simplifying Extended String Constraints in SMT CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis Invertibility Conditions for Floating-Point Formulas
Rieg, Lionel	Integrating Formal Schedulability Analysis into a Verifed OS Kernel
Roohi, Nima	Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
Roussanaly, Victor	Abstraction Refinement Algorithms for Timed Automata
Roveri, Marco	Extending nuXmv with Timed Transition Systems and Timed Temporal Properties
Rozier, Kristin Y.	Satisfiability Checking for Mission-Time LTL
Ruemmer, Philipp	Probabilistic Bisimulation for Parameterized Systems
Rungta, Neha	Reachability Analysis for AWS-based Networks
S
Sagiv, Mooly	Inferring Inductive Invariants from Phase Structures
Sammartino, Matteo	Symbolic Register Automata
Sanan, David	Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS
Sanchez, Cesar	Verifying Hyperliveness
Sankur, Ocan	Abstraction Refinement Algorithms for Timed Automata Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach
Santolucito, Mark	Temporal Stream Logic: Synthesis beyond the Bools
Schilling, Christian	Membership-based Synthesis of Linear Hybrid Automata
Schledjewski, Malte	StreamLAB: Stream-based Monitoring of Cyber-Physical Systems
Schwenger, Maximilian	StreamLAB: Stream-based Monitoring of Cyber-Physical Systems
Seshia, Sanjit A.	Flexible Computational Pipelines for Robust Abstraction-based Control Synthesis Verifai: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems
Sewell, Peter	Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C
Shah, Parth	The Marabou Framework for Verification and Analysis of Deep Neural Networks
Shao, Zhong	Integrating Formal Schedulability Analysis into a Verifed OS Kernel
Sharma, Rahul	Overfitting in Synthesis: Theory and Practice
Shemer, Ron	Property Directed Self Composition
Shoham, Sharon	Verification of Threshold-based Distributed Algorithms by Decomposition to Decidable Logics Property Directed Self Composition Inferring Inductive Invariants from Phase Structures
Siegel, Stephen F.	What's wrong with on-the-fly partial order reduction
Silva, Alexandra	Symbolic Register Automata
Silverman, Jake	Loop Summarization with Rational Vector Addition Systems
Sizemore, John	Reachability Analysis for AWS-based Networks
Solar-Lezama, Armando	Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
Srinivasan, Preethi	Reachability Analysis for AWS-based Networks
Srivathsan, B	Fast algorithms for handling diagonal constraints in timed automata
Stalzer, Mark	Reachability Analysis for AWS-based Networks
Stenger, Marvin	StreamLAB: Stream-based Monitoring of Cyber-Physical Systems
Strejček, Jan	Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors
Subotic, Pavle	Reachability Analysis for AWS-based Networks
T
Tatlock, Zachary	Icing: Supporting Fast-math Style Optimizations in a Verified Compiler
Tentrup, Leander	Verifying Hyperliveness StreamLAB: Stream-based Monitoring of Cyber-Physical Systems
Thakoor, Shantanu	The Marabou Framework for Verification and Analysis of Deep Neural Networks
Tinelli, Cesare	High-Level Abstractions for Simplifying Extended String Constraints in SMT CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis Invertibility Conditions for Floating-Point Formulas
Tizpaz Niari, Saeid	Quantitative Mitigation of Timing Side Channels
Tonetta, Stefano	Extending nuXmv with Timed Transition Systems and Timed Temporal Properties
Torfah, Hazem	Synthesizing Approximate Implementations for Unrealizable Specifications StreamLAB: Stream-based Monitoring of Cyber-Physical Systems
Tripakis, Stavros	Automated Synthesis of Secure Platform Mappings
Trivedi, Ashutosh	Quantitative Mitigation of Timing Side Channels
V
Vandikas, Anthony	Automated Hypersafety Verification
Vardi, Moshe	Safety and co-safety comparator automata for discounted-sum inclusion Satisfiability Checking for Mission-Time LTL
Varming, Carsten	Reachability Analysis for AWS-based Networks
Vazquez-Chanlatte, Marcell	Verifai: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems
Vediramana Krishnan, Hari Govind	Interpolating Strong Induction
Vizel, Yakir	Interpolating Strong Induction Property Directed Self Composition
Volkova, Anastasia	Sound Approximation of Programs with Elementary Functions
W
Waga, Masaki	Symbolic Monitoring against Specifications Parametric in Time and Data
Wahl, Thomas	Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers
Walker, David	Efficient verification of network fault tolerance via counterexample-guided refinement
Wang, Shuling	Formal verification of quantum algorithms using quantum Hoare logic
Wang, Yu	Security-Aware Synthesis Using Delayed-Action Games
Weininger, Maximilian	PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
Whaley, Blake	Reachability Analysis for AWS-based Networks
Widder, Josef	Communication-closed asynchronous protocols
Wies, Thomas	Clock Bound Repair for Timed Systems
Wilcox, James R.	Inferring Inductive Invariants from Phase Structures
Wu, Haoze	The Marabou Framework for Verification and Analysis of Deep Neural Networks
Wu, Yiwen	Reachability Analysis for AWS-based Networks
X
Xu, Xiao	Alternating Automata Modulo First Order Theories
Xue, Bai	Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations
Y
Ying, Mingsheng	Formal verification of quantum algorithms using quantum Hoare logic
Ying, Shenggang	Formal verification of quantum algorithms using quantum Hoare logic
Z
Zeleznik, Luka	Membership-based Synthesis of Linear Hybrid Automata
Zeljic, Aleksandar	The Marabou Framework for Verification and Analysis of Deep Neural Networks
Zennou, Rachid	Gradual Consistency Checking
Zhan, Bohua	Formal verification of quantum algorithms using quantum Hoare logic
Zhan, Naijun	Formal verification of quantum algorithms using quantum Hoare logic Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations
Zhang, Zhen	STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis
Zhang, Zhenya	Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification
Zhao, Yongwang	Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS
Zheng, Hao	STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis

Disclaimer | Powered by EasyChair Smart Program