VSL 2014: VIENNA SUMMER OF LOGIC 2014

This page contains an index consisting of author-provided keywords.

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

Disclaimer | Powered by EasyChair Smart Program