CAV 2014 LNCS PROCEEDINGS: AUTHOR INDEX

Papers Papers with Abstracts Preface Author Index Keyword Index

Shortcuts: A B C D E F G H I J K L M N O P Q R S T V W Y Z Č

A
Abdulla, Parosh Aziz	String Constraints for Verification (PDF, talk)
Aiken, Alex	From Invariant Checking to Invariant Inference Using Randomized Search (PDF, talk)
Alglave, Jade	Don't sit on the fence: A static analysis approach to automatic fence insertion (PDF, talk)
Alur, Rajeev	The First Syntax-Guided Synthesis Competition (SyGuS-COMP 2014) (PDF, talk) Symbolic Visibly Pushdown Automata (PDF, talk)
Atig, Mohamed Faouzi	String Constraints for Verification (PDF, talk)
B
Bacchus, Fahiem	Solving Games without Controllable Predecessor (PDF, talk)
Bansal, Kshitij	A Tale of Two Solver: Eager and Lazy Approaches to Bit-vectors (PDF, talk)
Bardsley, Ethel	Engineering a Static Verification Tool for GPU Kernels (PDF, talk)
Barrett, Clark	A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (PDF, talk) A Tale of Two Solver: Eager and Lazy Approaches to Bit-vectors (PDF, talk)
Bereg, Sergey	Monadic Decomposition (PDF, talk)
Betts, Adam	Engineering a Static Verification Tool for GPU Kernels (PDF, talk)
Beyer, Dirk	Software Verification in the Google App-Engine Cloud (PDF, talk)
Biere, Armin	Hardware Model Checking Competition CAV 2014 Edition (PDF, talk)
Bingham, Jesse	Verifying Relative Error Bounds using Symbolic Simulation (PDF, talk)
Birgmeier, Johannes	Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) (PDF, talk)
Bjorner, Nikolaj	Property-Directed Shape Analysis (PDF, talk) Monadic Decomposition (PDF, talk)
Bloem, Roderick	SYNTCOMP - Synthesis Competition for Reactive Systems (PDF, talk)
Bosnacki, Dragan	GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components (PDF, talk)
Bozianu, Rodica	Safraless Synthesis for Epistemic Temporal Specifications (PDF, talk)
Bradley, Aaron R.	Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) (PDF, talk)
Brazdil, Tomas	Minimizing Running Costs in Consumption Systems (PDF, talk)
C
Cavada, Roberto	The nuXmv Symbolic Model Checker (PDF, talk)
Cerny, Pavol	Regression-free Synthesis for Concurrency (PDF, talk)
Chaki, Sagar	SMT-based Model Checking for Recursive Programs (PDF, talk)
Chang, Bor-Yuh Evan	QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers (PDF, talk)
Chatterjee, Krishnendu	CEGAR for Qualitative Analysis of Probabilistic Systems (PDF, talk)
Chaudhuri, Swarat	Optimal Guard Synthesis for Memory Safety (PDF, talk)
Chen, Yu-Fang	String Constraints for Verification (PDF, talk)
Cheng, Chih-Hong	G4LTL-ST: Automatic Generation of PLC Programs (PDF, talk)
Chin, Wei-Ngan	Shape Analysis via Second-Order Bi-Abduction (PDF, talk)
Chmelík, Martin	CEGAR for Qualitative Analysis of Probabilistic Systems (PDF, talk)
Chong, Nathan	Engineering a Static Verification Tool for GPU Kernels (PDF, talk)
Chowdhury, Omar	Temporal Mode-Checking for Runtime Monitoring of Privacy Policies (PDF, talk)
Cimatti, Alessandro	The nuXmv Symbolic Model Checker (PDF, talk) Verifying LTL properties of hybrid systems with K-liveness (PDF, talk)
Cleaveland, Rance	Automated Testing (PDF, talk)
Collingbourne, Peter	Engineering a Static Verification Tool for GPU Kernels (PDF, talk)
Cook, Byron	Finding instability in biological models (PDF, talk)
Cox, Arlen	QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers (PDF, talk)
D
D'Antoni, Loris	Symbolic Visibly Pushdown Automata (PDF, talk)
Daca, Przemyslaw	CEGAR for Qualitative Analysis of Probabilistic Systems (PDF, talk)
Datta, Anupam	Temporal Mode-Checking for Runtime Monitoring of Privacy Policies (PDF, talk)
Deligiannis, Pantazis	Engineering a Static Verification Tool for GPU Kernels (PDF, talk)
Deters, Morgan	A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (PDF, talk)
Dillig, Isil	Optimal Guard Synthesis for Memory Safety (PDF, talk)
Dillig, Thomas	Optimal Guard Synthesis for Memory Safety (PDF, talk)
Dima, Catalin	Safraless Synthesis for Epistemic Temporal Specifications (PDF, talk)
Donaldson, Alastair	Engineering a Static Verification Tool for GPU Kernels (PDF, talk)
Dorigatti, Michele	The nuXmv Symbolic Model Checker (PDF, talk)
Dresler, Georg	Software Verification in the Google App-Engine Cloud (PDF, talk)
Dutertre, Bruno	Yices 2.2 (PDF, talk)
E
Ehlers, Rüdiger	SYNTCOMP - Synthesis Competition for Reactive Systems (PDF, talk)
Eldib, Hassan	Synthesis of Masking Countermeasures against Side Channel Attacks (PDF, talk)
Eloussi, Lamyaa	Regression Test Selection for Distributed Software Histories (PDF, talk)
Emmi, Michael	SMACK: Decoupling Source Language Details from Verifier Implementations (PDF, talk)
Esparza, Javier	From LTL to Deterministic Automata: A Safraless Compositional Approach (PDF, talk) An SMT-based Approach to Coverability Analysis (PDF, talk)
F
Fan, Chuchu	Invariant verification of nonlinear hybrid automata networks of cardiac cells (PDF, talk)
Ferrara, Anna Lisa	VAC - Verifier of Administrative Role-based Access Control Policies (PDF, talk)
Filiot, Emmanuel	Safraless Synthesis for Epistemic Temporal Specifications (PDF, talk)
Filliatre, Jean-Christophe	The Spirit of Ghost Code (PDF, talk)
Finkbeiner, Bernd	Causal Termination of Multi-threaded Programs (PDF, talk)
Fischer, Bernd	Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization (PDF, talk)
Fisher, Jasmin	Finding instability in biological models (PDF, talk)
Fisman, Dana	The First Syntax-Guided Synthesis Competition (SyGuS-COMP 2014) (PDF, talk)
G
Garg, Deepak	Temporal Mode-Checking for Runtime Monitoring of Privacy Policies (PDF, talk)
Garg, Pranav	ICE: A Robust Learning Framework for Synthesizing Invariants (PDF, talk)
Gherghina, Cristian	Shape Analysis via Second-Order Bi-Abduction (PDF, talk)
Gligoric, Milos	Regression Test Selection for Distributed Software Histories (PDF, talk)
Gondelman, Léon	The Spirit of Ghost Code (PDF, talk)
Griggio, Alberto	The nuXmv Symbolic Model Checker (PDF, talk) Verifying LTL properties of hybrid systems with K-liveness (PDF, talk)
Gurfinkel, Arie	SMT-based Model Checking for Recursive Programs (PDF, talk) Interpolating Property Directed Reachability (PDF, talk)
H
Hadarean, Liana	A Tale of Two Solver: Eager and Lazy Approaches to Bit-vectors (PDF, talk)
Hagemann, Willem	Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections (PDF, talk)
Hall, Benjamin	Finding instability in biological models (PDF, talk)
Hamadi, Youssef	Analyzing and Synthesizing Genomic Logic Functions (PDF, talk)
Hansen, Henri	Diamonds are a Girl's Best Friend: Partial Order Reduction for Timed Automata With Abstractions (PDF, talk)
Heizmann, Matthias	Termination Analysis by Learning Terminating Programs (PDF, talk)
Heljanko, Keijo	Hardware Model Checking Competition CAV 2014 Edition (PDF, talk)
Henzinger, Thomas	Regression-free Synthesis for Concurrency (PDF, talk)
Hoenicke, Jochen	Termination Analysis by Learning Terminating Programs (PDF, talk)
Holik, Lukas	String Constraints for Verification (PDF, talk)
Huang, Chung-Hao	G4LTL-ST: Automatic Generation of PLC Programs (PDF, talk)
Huang, Zhenqi	Invariant verification of nonlinear hybrid automata networks of cardiac cells (PDF, talk)
I
Inverso, Omar	Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization (PDF, talk)
Ishtiaq, Samin	Finding instability in biological models (PDF, talk)
Itzhaky, Shachar	Property-Directed Shape Analysis (PDF, talk)
J
Jacobs, Swen	SYNTCOMP - Synthesis Competition for Reactive Systems (PDF, talk)
Jia, Limin	Temporal Mode-Checking for Runtime Monitoring of Privacy Policies (PDF, talk)
Jovanović, Dejan	A Tale of Two Solver: Eager and Lazy Approaches to Bit-vectors (PDF, talk)
Juniwal, Garvit	Finding instability in biological models (PDF, talk)
K
Kanav, Sudeep	A Conference Management System with Verified Document Confidentiality (PDF, talk)
Katoen, Joost-Pieter	GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components (PDF, talk)
Ketema, Jeroen	Engineering a Static Verification Tool for GPU Kernels (PDF, talk)
Klaska, David	Minimizing Running Costs in Consumption Systems (PDF, talk)
Komuravelli, Anvesh	SMT-based Model Checking for Recursive Programs (PDF, talk)
Kretinsky, Jan	From LTL to Deterministic Automata: A Safraless Compositional Approach (PDF, talk)
Kroening, Daniel	Don't sit on the fence: A static analysis approach to automatic fence insertion (PDF, talk)
Kucera, Antonin	Minimizing Running Costs in Consumption Systems (PDF, talk)
Kugler, Hillel	Analyzing and Synthesizing Genomic Logic Functions (PDF, talk)
Kuncak, Viktor	Symbolic Resource Bound Inference for Functional Programs (PDF, talk)
Kupriyanov, Andrey	Causal Termination of Multi-threaded Programs (PDF, talk)
Kwiatkowska, Marta	Invariant verification of nonlinear hybrid automata networks of cardiac cells (PDF, talk)
L
La Torre, Salvatore	Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization (PDF, talk)
Lammich, Peter	A Conference Management System with Verified Document Confidentiality (PDF, talk)
Larraz, Daniel	Proving Non-termination Using Max-SMT (PDF, talk)
Le, Quang Loc	Shape Analysis via Second-Order Bi-Abduction (PDF, talk)
Ledesma-Garza, Ruslán	An SMT-based Approach to Coverability Analysis (PDF, talk)
Lee, Suho	Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction (PDF, talk)
Legg, Alexander	Solving Games without Controllable Predecessor (PDF, talk)
Lesani, Mohsen	Automatic Atomicity Verification for Clients of Concurrent Data Structures (PDF, talk)
Leslie-Hurd, Joe	Verifying Relative Error Bounds using Symbolic Simulation (PDF, talk)
Liang, Tianyi	A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (PDF, talk)
Liew, Dan	Engineering a Static Verification Tool for GPU Kernels (PDF, talk)
Lin, Shang-Wei	Diamonds are a Girl's Best Friend: Partial Order Reduction for Timed Automata With Abstractions (PDF, talk)
Lincoln, Patrick	A Nonlinear Real Arithmetic Fragment (PDF, talk)
Liu, Yang	Diamonds are a Girl's Best Friend: Partial Order Reduction for Timed Automata With Abstractions (PDF, talk)
Loding, Christof	ICE: A Robust Learning Framework for Synthesizing Invariants (PDF, talk)
Lomuscio, Alessio	MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications (PDF, talk)
M
Madhavan, Ravichandhran	Symbolic Resource Bound Inference for Functional Programs (PDF, talk)
Madhusudan, P.	ICE: A Robust Learning Framework for Synthesizing Invariants (PDF, talk) VAC - Verifier of Administrative Role-based Access Control Policies (PDF, talk)
Majumdar, Rupak	Regression Test Selection for Distributed Software Histories (PDF, talk) An SMT-based Approach to Coverability Analysis (PDF, talk)
Marinov, Darko	Regression Test Selection for Distributed Software Histories (PDF, talk)
Mariotti, Alessandro	The nuXmv Symbolic Model Checker (PDF, talk)
McMillan, Kenneth	Lazy Annotation Revisited (PDF, talk)
Mereacre, Alexandru	Invariant verification of nonlinear hybrid automata networks of cardiac cells (PDF, talk)
Meyer, Philipp	An SMT-based Approach to Coverability Analysis (PDF, talk)
Micheli, Andrea	The nuXmv Symbolic Model Checker (PDF, talk)
Millstein, Todd	Automatic Atomicity Verification for Clients of Concurrent Data Structures (PDF, talk)
Mitra, Sayan	Invariant verification of nonlinear hybrid automata networks of cardiac cells (PDF, talk)
Mogavero, Fabio	MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications (PDF, talk)
Monniaux, David	How do we get Inductive Invariants? (PDF, talk)
Mover, Sergio	The nuXmv Symbolic Model Checker (PDF, talk) Verifying LTL properties of hybrid systems with K-liveness (PDF, talk)
Murano, Aniello	MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications (PDF, talk)
N
Nachmanson, Lev	Monadic Decomposition (PDF, talk)
Nadel, Alexander	Bit-Vector Rewriting with Automatic Rule Generation (PDF, talk)
Narodytska, Nina	Solving Games without Controllable Predecessor (PDF, talk)
Neider, Daniel	ICE: A Robust Learning Framework for Synthesizing Invariants (PDF, talk)
Nguyen, Truc L.	VAC - Verifier of Administrative Role-based Access Control Policies (PDF, talk)
Nguyen, Truong Khanh	Diamonds are a Girl's Best Friend: Partial Order Reduction for Timed Automata With Abstractions (PDF, talk)
Niksic, Filip	An SMT-based Approach to Coverability Analysis (PDF, talk)
Nimal, Vincent	Don't sit on the fence: A static analysis approach to automatic fence insertion (PDF, talk)
Nimkar, Kaustubh	Proving Non-termination Using Max-SMT (PDF, talk)
Novotný, Petr	Minimizing Running Costs in Consumption Systems (PDF, talk)
O
Oliveras, Albert	Proving Non-termination Using Max-SMT (PDF, talk)
P
Palsberg, Jens	Automatic Atomicity Verification for Clients of Concurrent Data Structures (PDF, talk)
Paoletti, Nicola	Analyzing and Synthesizing Genomic Logic Functions (PDF, talk)
Parlato, Gennaro	VAC - Verifier of Administrative Role-based Access Control Policies (PDF, talk) Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization (PDF, talk)
Paskevich, Andrei	The Spirit of Ghost Code (PDF, talk)
Piskac, Ruzica	Automating Separation Logic with Trees and Data (PDF, talk)
Piterman, Nir	Finding instability in biological models (PDF, talk)
Podelski, Andreas	Termination Analysis by Learning Terminating Programs (PDF, talk)
Poetzl, Daniel	Don't sit on the fence: A static analysis approach to automatic fence insertion (PDF, talk)
Popescu, Andrei	A Conference Management System with Verified Document Confidentiality (PDF, talk)
Q
Qadeer, Shaz	Engineering a Static Verification Tool for GPU Kernels (PDF, talk)
Qin, Shengchao	Shape Analysis via Second-Order Bi-Abduction (PDF, talk)
R
Radhakrishna, Arjun	Regression-free Synthesis for Concurrency (PDF, talk)
Rakamaric, Zvonimir	SMACK: Decoupling Source Language Details from Verifier Implementations (PDF, talk)
Reps, Thomas	Property-Directed Shape Analysis (PDF, talk)
Reummer, Philipp	String Constraints for Verification (PDF, talk)
Reynolds, Andrew	A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (PDF, talk)
Rezine, Ahmed	String Constraints for Verification (PDF, talk)
Rodríguez-Carbonell, Enric	Proving Non-termination Using Max-SMT (PDF, talk)
Roveri, Marco	The nuXmv Symbolic Model Checker (PDF, talk)
Rubio, Albert	Proving Non-termination Using Max-SMT (PDF, talk)
Ruess, Harald	G4LTL-ST: Automatic Generation of PLC Programs (PDF, talk)
Ryzhyk, Leonid	Solving Games without Controllable Predecessor (PDF, talk)
Ryzhyk, Leonid	Regression-free Synthesis for Concurrency (PDF, talk)
S
Sagiv, Mooly	Property-Directed Shape Analysis (PDF, talk)
Sakallah, Karem A.	Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction (PDF, talk)
Sanchez, Alejandro	LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes (PDF, talk)
Sanchez, Cesar	LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes (PDF, talk)
Sankaranarayanan, Sriram	QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers (PDF, talk)
Sharma, Rahul	From Invariant Checking to Invariant Inference Using Randomized Search (PDF, talk)
Sharma, Rohan	Regression Test Selection for Distributed Software Histories (PDF, talk)
Singh, Rishab	The First Syntax-Guided Synthesis Competition (SyGuS-COMP 2014) (PDF, talk)
Sinn, Moritz	A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis (PDF, talk)
Solar-Lezama, Armando	The First Syntax-Guided Synthesis Competition (SyGuS-COMP 2014) (PDF, talk)
Somenzi, Fabio	Hardware Model Checking (PDF, talk)
Stattelmann, Stefan	G4LTL-ST: Automatic Generation of PLC Programs (PDF, talk)
Stenman, Jari	String Constraints for Verification (PDF, talk)
Sun, Jun	Diamonds are a Girl's Best Friend: Partial Order Reduction for Timed Automata With Abstractions (PDF, talk)
T
Tarrach, Thorsten	Regression-free Synthesis for Concurrency (PDF, talk)
Thakur, Aditya	Property-Directed Shape Analysis (PDF, talk)
Tinelli, Cesare	A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (PDF, talk) A Tale of Two Solver: Eager and Lazy Approaches to Bit-vectors (PDF, talk)
Tiwari, Ashish	A Nonlinear Real Arithmetic Fragment (PDF, talk)
Tomasco, Ermenegildo	Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization (PDF, talk)
Tonetta, Stefano	The nuXmv Symbolic Model Checker (PDF, talk) Verifying LTL properties of hybrid systems with K-liveness (PDF, talk)
V
Veanes, Margus	Monadic Decomposition (PDF, talk)
Veith, Helmut	A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis (PDF, talk)
Vizel, Yakir	Interpolating Property Directed Reachability (PDF, talk)
Voronkov, Andrei	AVATAR: The New Architecture for First-Order Theorem Provers (PDF, talk)
W
Walker, Adam	Solving Games without Controllable Predecessor (PDF, talk)
Wang, Chao	Synthesis of Masking Countermeasures against Side Channel Attacks (PDF, talk)
Weissenbacher, Georg	Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) (PDF, talk)
Wendler, Philipp	Software Verification in the Google App-Engine Cloud (PDF, talk)
Wies, Thomas	Automating Separation Logic with Trees and Data (PDF, talk)
Wijs, Anton	GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components (PDF, talk)
Winfree, Erik	Designing and Verifying Molecular Circuits and Systems Made of DNA (PDF, talk)
Wintersteiger, Christoph M.	Analyzing and Synthesizing Genomic Logic Functions (PDF, talk)
Y
Yordanov, Boyan	Analyzing and Synthesizing Genomic Logic Functions (PDF, talk)
Z
Zufferey, Damien	Automating Separation Logic with Trees and Data (PDF, talk)
Zuleger, Florian	A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis (PDF, talk)
Č
Čermák, Petr	MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications (PDF, talk)