CAV 2014 LNCS PROCEEDINGS: KEYWORD INDEX

Papers Papers with Abstracts Preface Author Index Keyword Index

Shortcuts: A B C D E F G H I K L M N P Q R S T U V W X

A
Abductive Reasoning	Optimal Guard Synthesis for Memory Safety (PDF, talk)
abstract domain	QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers (PDF, talk)
abstract domain combinator	QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers (PDF, talk)
abstract interpretation	QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers (PDF, talk)
Abstraction refinement	SMT-based Model Checking for Recursive Programs (PDF, talk) Diamonds are a Girl's Best Friend: Partial Order Reduction for Timed Automata With Abstractions (PDF, talk) G4LTL-ST: Automatic Generation of PLC Programs (PDF, talk)
abstraction-refinement	Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) (PDF, talk)
access control	VAC - Verifier of Administrative Role-based Access Control Policies (PDF, talk)
amortized complexity	A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis (PDF, talk)
Approximate Reachability	Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction (PDF, talk)
approximation	SMT-based Model Checking for Recursive Programs (PDF, talk)
ATL and ATL*	CEGAR for Qualitative Analysis of Probabilistic Systems (PDF, talk)
Atomicity	Automatic Atomicity Verification for Clients of Concurrent Data Structures (PDF, talk)
Automata	From LTL to Deterministic Automata: A Safraless Compositional Approach (PDF, talk)
Automatic verification	VAC - Verifier of Administrative Role-based Access Control Policies (PDF, talk)
B
Bi-Abduction	Shape Analysis via Second-Order Bi-Abduction (PDF, talk)
Biological Networks	Invariant verification of nonlinear hybrid automata networks of cardiac cells (PDF, talk)
Biological Systems	Analyzing and Synthesizing Genomic Logic Functions (PDF, talk)
biology	Finding instability in biological models (PDF, talk)
bisimulation	The Spirit of Ghost Code (PDF, talk)
Bit-vector	Bit-Vector Rewriting with Automatic Rule Generation (PDF, talk)
Bit-vector Preprocessing	Bit-Vector Rewriting with Automatic Rule Generation (PDF, talk)
bit-vectors	A Tale of Two Solver: Eager and Lazy Approaches to Bit-vectors (PDF, talk)
bmc	SMT-based Model Checking for Recursive Programs (PDF, talk)
Bound Analysis	A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis (PDF, talk)
bounded model checking	Lazy Annotation Revisited (PDF, talk) Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization (PDF, talk)
Büchi automata	Termination Analysis by Learning Terminating Programs (PDF, talk)
C
Causality	Causal Termination of Multi-threaded Programs (PDF, talk)
CEGAR	CEGAR for Qualitative Analysis of Probabilistic Systems (PDF, talk)
Cloud Computing	Software Verification in the Google App-Engine Cloud (PDF, talk)
compiler intermediate representation	SMACK: Decoupling Source Language Details from Verifier Implementations (PDF, talk)
concurrency	Regression-free Synthesis for Concurrency (PDF, talk) Causal Termination of Multi-threaded Programs (PDF, talk)
Concurrent Data Structures	Automatic Atomicity Verification for Clients of Concurrent Data Structures (PDF, talk)
Concurrent datatypes	LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes (PDF, talk)
Concurrent programs	Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization (PDF, talk)
conference management system	A Conference Management System with Verified Document Confidentiality (PDF, talk)
confidentiality	A Conference Management System with Verified Document Confidentiality (PDF, talk)
constraint solving	Symbolic Resource Bound Inference for Functional Programs (PDF, talk)
controller synthesis	Minimizing Running Costs in Consumption Systems (PDF, talk)
convex hull	Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections (PDF, talk)
countermeasures	Synthesis of Masking Countermeasures against Side Channel Attacks (PDF, talk)
coverability problem	An SMT-based Approach to Coverability Analysis (PDF, talk)
Craig interpolation	Lazy Annotation Revisited (PDF, talk)
D
Datapath Abstraction	Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction (PDF, talk)
decision procedure	String Constraints for Verification (PDF, talk)
decision procedures	LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes (PDF, talk) A Tale of Two Solver: Eager and Lazy Approaches to Bit-vectors (PDF, talk) Automating Separation Logic with Trees and Data (PDF, talk) A Nonlinear Real Arithmetic Fragment (PDF, talk)
declassification	A Conference Management System with Verified Document Confidentiality (PDF, talk)
deductive program verification	The Spirit of Ghost Code (PDF, talk)
deductive verification	Automating Separation Logic with Trees and Data (PDF, talk)
determinization	From LTL to Deterministic Automata: A Safraless Compositional Approach (PDF, talk)
Device Drivers	Regression-free Synthesis for Concurrency (PDF, talk)
differential power analysis	Synthesis of Masking Countermeasures against Side Channel Attacks (PDF, talk)
distributed version control systems	Regression Test Selection for Distributed Software Histories (PDF, talk)
DPLL	AVATAR: The New Architecture for First-Order Theorem Provers (PDF, talk)
DPLL(T)	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)
E
energy games	Minimizing Running Costs in Consumption Systems (PDF, talk)
Engineering	Engineering a Static Verification Tool for GPU Kernels (PDF, talk)
epistemic temporal specification	Safraless Synthesis for Epistemic Temporal Specifications (PDF, talk)
F
Finite and Infinite Transition Systems	The nuXmv Symbolic Model Checker (PDF, talk)
First-order temporal logic	Temporal Mode-Checking for Runtime Monitoring of Privacy Policies (PDF, talk)
first-order theorem proving	AVATAR: The New Architecture for First-Order Theorem Provers (PDF, talk)
floating point	Verifying Relative Error Bounds using Symbolic Simulation (PDF, talk)
Floyd-Hoare logic	Termination Analysis by Learning Terminating Programs (PDF, talk)
formal methods	Software Verification in the Google App-Engine Cloud (PDF, talk)
Formal Verification	Verifying Relative Error Bounds using Symbolic Simulation (PDF, talk) MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications (PDF, talk)
G
games	Safraless Synthesis for Epistemic Temporal Specifications (PDF, talk) CEGAR for Qualitative Analysis of Probabilistic Systems (PDF, talk)
ghost code	The Spirit of Ghost Code (PDF, talk)
git	Regression Test Selection for Distributed Software Histories (PDF, talk)
GPU	Engineering a Static Verification Tool for GPU Kernels (PDF, talk)
graph decomposition	GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components (PDF, talk)
graphics processing units	GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components (PDF, talk)
H
hardware	Verifying Relative Error Bounds using Symbolic Simulation (PDF, talk)
heap structures	Automating Separation Logic with Trees and Data (PDF, talk)
horn	SMT-based Model Checking for Recursive Programs (PDF, talk)
hybrid automata	Verifying LTL properties of hybrid systems with K-liveness (PDF, talk)
hybrid systems	Invariant verification of nonlinear hybrid automata networks of cardiac cells (PDF, talk)
I
ic3	SMT-based Model Checking for Recursive Programs (PDF, talk) Interpolating Property Directed Reachability (PDF, talk)
IC3/PDR	Property-Directed Shape Analysis (PDF, talk)
imperfect information	Safraless Synthesis for Epistemic Temporal Specifications (PDF, talk)
inductive invariant	Property-Directed Shape Analysis (PDF, talk)
inductive synthesis	Synthesis of Masking Countermeasures against Side Channel Attacks (PDF, talk)
Industrial automation	G4LTL-ST: Automatic Generation of PLC Programs (PDF, talk)
information-flow security	A Conference Management System with Verified Document Confidentiality (PDF, talk)
instability	Finding instability in biological models (PDF, talk)
intermediate verification language	SMACK: Decoupling Source Language Details from Verifier Implementations (PDF, talk)
Interpolation	Interpolating Property Directed Reachability (PDF, talk) Termination Analysis by Learning Terminating Programs (PDF, talk)
intersection	Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections (PDF, talk)
invariant synthesis	ICE: A Robust Learning Framework for Synthesizing Invariants (PDF, talk)
Invariants	Invariant verification of nonlinear hybrid automata networks of cardiac cells (PDF, talk)
K
k-liveness	Verifying LTL properties of hybrid systems with K-liveness (PDF, talk)
L
Lazy Annotation	Lazy Annotation Revisited (PDF, talk)
learning	ICE: A Robust Learning Framework for Synthesizing Invariants (PDF, talk)
Lexicographic Ranking Function	A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis (PDF, talk)
Linear Algebra	A Nonlinear Real Arithmetic Fragment (PDF, talk)
linear constraints	An SMT-based Approach to Coverability Analysis (PDF, talk)
Linear Temporal Logic	From LTL to Deterministic Automata: A Safraless Compositional Approach (PDF, talk) G4LTL-ST: Automatic Generation of PLC Programs (PDF, talk)
linear transformation	Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections (PDF, talk)
Linearizability	Automatic Atomicity Verification for Clients of Concurrent Data Structures (PDF, talk)
logic	String Constraints for Verification (PDF, talk)
loop invariants	From Invariant Checking to Invariant Inference Using Randomized Search (PDF, talk)
LTL	Verifying LTL properties of hybrid systems with K-liveness (PDF, talk)
M
Many core	Engineering a Static Verification Tool for GPU Kernels (PDF, talk)
Max-SMT	Proving Non-termination Using Max-SMT (PDF, talk)
MCMC	From Invariant Checking to Invariant Inference Using Randomized Search (PDF, talk)
mean payoff	Minimizing Running Costs in Consumption Systems (PDF, talk)
memory fence synthesis	Don't sit on the fence: A static analysis approach to automatic fence insertion (PDF, talk)
memory safety	Optimal Guard Synthesis for Memory Safety (PDF, talk)
Minkowski sum	Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections (PDF, talk)
Mode checking	Temporal Mode-Checking for Runtime Monitoring of Privacy Policies (PDF, talk)
model checking	SMT-based Model Checking for Recursive Programs (PDF, talk) Interpolating Property Directed Reachability (PDF, talk) Software Verification in the Google App-Engine Cloud (PDF, talk) MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications (PDF, talk) Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) (PDF, talk)
Model Synthesis	Analyzing and Synthesizing Genomic Logic Functions (PDF, talk)
Multi-agent systems	MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications (PDF, talk)
N
Nested Words	Symbolic Visibly Pushdown Automata (PDF, talk)
non-interference	The Spirit of Ghost Code (PDF, talk)
nonlinear real arithmetic	A Nonlinear Real Arithmetic Fragment (PDF, talk)
Nontermination	Proving Non-termination Using Max-SMT (PDF, talk)
P
parallel computing	GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components (PDF, talk)
Parametrized systems	LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes (PDF, talk)
partial order reduction	Diamonds are a Girl's Best Friend: Partial Order Reduction for Timed Automata With Abstractions (PDF, talk)
pdr	SMT-based Model Checking for Recursive Programs (PDF, talk)
perfect masking	Synthesis of Masking Countermeasures against Side Channel Attacks (PDF, talk)
Petri nets	An SMT-based Approach to Coverability Analysis (PDF, talk)
predicate abstraction	Property-Directed Shape Analysis (PDF, talk)
Privacy policy compliance	Temporal Mode-Checking for Runtime Monitoring of Privacy Policies (PDF, talk)
probabilistic systems	CEGAR for Qualitative Analysis of Probabilistic Systems (PDF, talk)
Program repair	Regression-free Synthesis for Concurrency (PDF, talk)
program synthesis	A Conference Management System with Verified Document Confidentiality (PDF, talk) Optimal Guard Synthesis for Memory Safety (PDF, talk) Regression-free Synthesis for Concurrency (PDF, talk)
program transformation	Don't sit on the fence: A static analysis approach to automatic fence insertion (PDF, talk)
program verification	Shape Analysis via Second-Order Bi-Abduction (PDF, talk) ICE: A Robust Learning Framework for Synthesizing Invariants (PDF, talk)
Programmable logic controllers	G4LTL-ST: Automatic Generation of PLC Programs (PDF, talk)
Property Directed Reachability	Interpolating Property Directed Reachability (PDF, talk)
property-driven	SMT-based Model Checking for Recursive Programs (PDF, talk)
Property-driven reachability	Lazy Annotation Revisited (PDF, talk)
Q
QBF	Solving Games without Controllable Predecessor (PDF, talk)
quantifier elimination	SMT-based Model Checking for Recursive Programs (PDF, talk)
quantifiers and theories	AVATAR: The New Architecture for First-Order Theorem Provers (PDF, talk)
Quasi-Invariants	Proving Non-termination Using Max-SMT (PDF, talk)
R
reachability analysis	Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections (PDF, talk)
reactive synthesis	Solving Games without Controllable Predecessor (PDF, talk)
realizability	Safraless Synthesis for Epistemic Temporal Specifications (PDF, talk)
recursion	SMT-based Model Checking for Recursive Programs (PDF, talk)
regression test selection	Regression Test Selection for Distributed Software Histories (PDF, talk)
relational	QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers (PDF, talk)
relative error	Verifying Relative Error Bounds using Symbolic Simulation (PDF, talk)
Rewriting	Bit-Vector Rewriting with Automatic Rule Generation (PDF, talk)
Runtime monitoring	Temporal Mode-Checking for Runtime Monitoring of Privacy Policies (PDF, talk)
S
SAT	Solving Games without Controllable Predecessor (PDF, talk) AVATAR: The New Architecture for First-Order Theorem Provers (PDF, talk)
SAT modulo theories	Lazy Annotation Revisited (PDF, talk)
SAT solving	A Nonlinear Real Arithmetic Fragment (PDF, talk)
Satifiability Modulo Theory	The nuXmv Symbolic Model Checker (PDF, talk)
Satisfiability Modulo Theories	Automating Separation Logic with Trees and Data (PDF, talk) Yices 2.2 (PDF, talk)
Scalable Unbounded Verification	Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction (PDF, talk)
Sea Urchin Development	Analyzing and Synthesizing Genomic Logic Functions (PDF, talk)
Security	Synthesis of Masking Countermeasures against Side Channel Attacks (PDF, talk) VAC - Verifier of Administrative Role-based Access Control Policies (PDF, talk)
security vulnerabilities	String Constraints for Verification (PDF, talk)
separation logic	Shape Analysis via Second-Order Bi-Abduction (PDF, talk)
Sequentialization	Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization (PDF, talk)
sets	QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers (PDF, talk)
shape analysis	Property-Directed Shape Analysis (PDF, talk) Shape Analysis via Second-Order Bi-Abduction (PDF, talk) Automating Separation Logic with Trees and Data (PDF, talk)
side channel attacks	Synthesis of Masking Countermeasures against Side Channel Attacks (PDF, talk)
Simulation and alternating simulation	CEGAR for Qualitative Analysis of Probabilistic Systems (PDF, talk)
SMT	SMT-based Model Checking for Recursive Programs (PDF, talk) Analyzing and Synthesizing Genomic Logic Functions (PDF, talk) Verifying LTL properties of hybrid systems with K-liveness (PDF, talk) An SMT-based Approach to Coverability Analysis (PDF, talk) Monadic Decomposition (PDF, talk) A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (PDF, talk) Bit-Vector Rewriting with Automatic Rule Generation (PDF, talk) A Tale of Two Solver: Eager and Lazy Approaches to Bit-vectors (PDF, talk)
SMT solvers	Synthesis of Masking Countermeasures against Side Channel Attacks (PDF, talk)
Software model checking	Lazy Annotation Revisited (PDF, talk) Termination Analysis by Learning Terminating Programs (PDF, talk)
Software synthesis	G4LTL-ST: Automatic Generation of PLC Programs (PDF, talk)
Software Verification	SMACK: Decoupling Source Language Details from Verifier Implementations (PDF, talk) Software Verification in the Google App-Engine Cloud (PDF, talk) Symbolic Resource Bound Inference for Functional Programs (PDF, talk)
Solver	Yices 2.2 (PDF, talk)
splittiing	AVATAR: The New Architecture for First-Order Theorem Provers (PDF, talk)
stability	Finding instability in biological models (PDF, talk)
state space analysis	GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components (PDF, talk)
Static Analysis	Don't sit on the fence: A static analysis approach to automatic fence insertion (PDF, talk) A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis (PDF, talk) Termination Analysis by Learning Terminating Programs (PDF, talk) Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) (PDF, talk)
Strategy Logic	MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications (PDF, talk)
String solvers	A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (PDF, talk)
strings	String Constraints for Verification (PDF, talk)
superposition calculus	AVATAR: The New Architecture for First-Order Theorem Provers (PDF, talk)
support function	Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections (PDF, talk)
Symbolic Automata	Symbolic Visibly Pushdown Automata (PDF, talk) Monadic Decomposition (PDF, talk)
Symbolic Model Checking	The nuXmv Symbolic Model Checker (PDF, talk)
symbolic orthogonal projections	Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections (PDF, talk)
symbolic simulation	Verifying Relative Error Bounds using Symbolic Simulation (PDF, talk)
Symbolic Time bounds	Symbolic Resource Bound Inference for Functional Programs (PDF, talk)
symbolic transducers	Monadic Decomposition (PDF, talk)
synthesis	Safraless Synthesis for Epistemic Temporal Specifications (PDF, talk)
T
Tableau	Causal Termination of Multi-threaded Programs (PDF, talk)
termination	Causal Termination of Multi-threaded Programs (PDF, talk)
termination analysis	A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis (PDF, talk) Termination Analysis by Learning Terminating Programs (PDF, talk)
theorem proving	A Conference Management System with Verified Document Confidentiality (PDF, talk)
Theory combination	Yices 2.2 (PDF, talk)
Theory of Strings	A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (PDF, talk)
timed verification	Diamonds are a Girl's Best Friend: Partial Order Reduction for Timed Automata With Abstractions (PDF, talk)
Tools	Engineering a Static Verification Tool for GPU Kernels (PDF, talk) Software Verification in the Google App-Engine Cloud (PDF, talk)
two-player games	Solving Games without Controllable Predecessor (PDF, talk)
type system	The Spirit of Ghost Code (PDF, talk)
U
unwinding relation	A Conference Management System with Verified Document Confidentiality (PDF, talk)
V
verification	From Invariant Checking to Invariant Inference Using Randomized Search (PDF, talk) String Constraints for Verification (PDF, talk) Engineering a Static Verification Tool for GPU Kernels (PDF, talk) Finding instability in biological models (PDF, talk) Invariant verification of nonlinear hybrid automata networks of cardiac cells (PDF, talk) Automatic Atomicity Verification for Clients of Concurrent Data Structures (PDF, talk) Causal Termination of Multi-threaded Programs (PDF, talk) Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) (PDF, talk)
Verification tools	LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes (PDF, talk)
Visibly Pushdown Languages	Symbolic Visibly Pushdown Automata (PDF, talk)
W
weak memory models	Don't sit on the fence: A static analysis approach to automatic fence insertion (PDF, talk)
X
XML Processing	Symbolic Visibly Pushdown Automata (PDF, talk)