VSL 2014: VIENNA SUMMER OF LOGIC 2014

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

Disclaimer | Powered by EasyChair Smart Program