Powered by
2013 European Joint Conferences on Theory and Practice of Software (ETAPS),
March 16–24, 2013,
Rome, Italy
TACAS 2013
Markov Chains
Mon, Mar 18, 11:00 - 12:30, Room B1 (Chair: Joost-Pieter Katoen)
On-the-Fly Exact Computation of Bisimilarity Distances
Radu Mardare
(Dept. of Mathematics and Computer Science, University of Udine, Italy, Italy; Dept. of Computer Science, Aalborg University, Denmark, Denmark)
@InProceedings{ETAPS13p1,
author = {Radu Mardare},
title = {On-the-Fly Exact Computation of Bisimilarity Distances},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
The Quest for Minimal Quotients for Probabilistic Automata
Lijun Zhang
(Saarland University, Germany; Universität der Bundeswehr München, Germany; Universität des Saarlandes, Germany; Technical University of Denmark, Denmark)
@InProceedings{ETAPS13p5,
author = {Lijun Zhang},
title = {The Quest for Minimal Quotients for Probabilistic Automata},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
LTL model checking of Interval Markov Chains
James Worrell
(Oxford University, UK; Oxford University, Computing Laboratory, UK)
@InProceedings{ETAPS13p9,
author = {James Worrell},
title = {LTL model checking of Interval Markov Chains},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Termination and Quantifier Elmination
Mon, Mar 18, 14:00 - 15:30, Room B1 (Chair: Saddek Bensalem)
Ramsey vs. lexicographic termination proving
Florian Zuleger
(Microsoft Research, UK; Cambridge University, UK; TU Wien, Austria)
@InProceedings{ETAPS13p13,
author = {Florian Zuleger},
title = {Ramsey vs. lexicographic termination proving},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Structural Counter Abstraction
Damien Zufferey
(New York University, USA; IST Austria, Austria)
@InProceedings{ETAPS13p17,
author = {Damien Zufferey},
title = {Structural Counter Abstraction},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
SAT/SMT
Mon, Mar 18, 16:00 - 18:00, Room B1 (Chair: Orna Grumberg)
The MathSAT5 SMT Solver
Roberto Sebastiani
(FBK-irst, Italy; FBK-IRST, Italy; DISI, University of Trento and FBK-IRST, Italy; DISI, University of Trento, Italy)
@InProceedings{ETAPS13p25,
author = {Roberto Sebastiani},
title = {The MathSAT5 SMT Solver},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Formula Preprocessing in MUS Extraction
Joao Marques-Silva
(Univesity College Dublin, Ireland; University of Helsinki, Finland; University College Dublin, Ireland)
@InProceedings{ETAPS13p29,
author = {Joao Marques-Silva},
title = {Formula Preprocessing in MUS Extraction},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Proof Tree Preserving Interpolation
Alexander Nutz
(University of Freiburg, Germany)
@InProceedings{ETAPS13p33,
author = {Alexander Nutz},
title = {Proof Tree Preserving Interpolation},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Asynchronous Multi-Core Incremental SAT Solving
Keijo Heljanko
(Aalto University School of Science and Technology, Finland; Aalto University, Finland)
@InProceedings{ETAPS13p37,
author = {Keijo Heljanko},
title = {Asynchronous Multi-Core Incremental SAT Solving},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Games & Synthesis and Process Algebra
Tue, Mar 19, 10:30 - 12:30, Room B1 (Chair: Barbara König)
Model-Checking Iterative Games
Farn Wang
(National Taiwan University, Taiwan; University of Liverpool, UK)
@InProceedings{ETAPS13p41,
author = {Farn Wang},
title = {Model-Checking Iterative Games},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Synthesis from LTL Specifications with Mean-Payoff Objectives
Jean-Francois Raskin
(UMONS, Belgium; University of Mons, Belgium; Universite Paris-Est Creteil, France; Universite Libre de Bruxelles, Belgium)
@InProceedings{ETAPS13p45,
author = {Jean-Francois Raskin},
title = {Synthesis from LTL Specifications with Mean-Payoff Objectives},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
PRISM-games: A Model Checker for Stochastic Multi-Player Games
Aistis Simaitis
(University of Oxford, UK; Oxford University, UK; University of Birmingham, UK)
@InProceedings{ETAPS13p49,
author = {Aistis Simaitis},
title = {PRISM-games: A Model Checker for Stochastic Multi-Player Games},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
PIC2LNT: Model Transformation for Model Checking an Applied Pi-calculus
Gwen Salaün
(INRIA Grenoble - Rhone-Alpes, France; Grenoble INP - INRIA - LIG, France)
@InProceedings{ETAPS13p53,
author = {Gwen Salaün},
title = {PIC2LNT: Model Transformation for Model Checking an Applied Pi-calculus},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Ins and outs of the mCRL2 toolset
Tim Willemse
(Eindhoven University of Technologoy, Netherlands; Eindhoven University of Technology, Netherlands; Eindhoven Universtiy of Technology, Netherlands)
@InProceedings{ETAPS13p57,
author = {Tim Willemse},
title = {Ins and outs of the mCRL2 toolset},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Pushdown Systems
Tue, Mar 19, 14:00 - 15:30, Room B1 (Chair: Axel Legay)
Analysis of Boolean Programs
Mihalis Yannakakis
(Microsoft Research, USA; Columbia University, USA)
@InProceedings{ETAPS13p61,
author = {Mihalis Yannakakis},
title = {Analysis of Boolean Programs},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Weighted Pushdown Systems with Indexed Weight Domains
Yasuhiko Minamide
(Faculty of Engineering, Information and Systems, University of Tsukuba, Japan)
@InProceedings{ETAPS13p65,
author = {Yasuhiko Minamide},
title = {Weighted Pushdown Systems with Indexed Weight Domains},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Underapproximation of Procedure Summaries for Integer Programs
Filip Konecny
(IMDEA Software Institute, Spain; Verimag, CNRS, France; Verimag, France)
@InProceedings{ETAPS13p69,
author = {Filip Konecny},
title = {Underapproximation of Procedure Summaries for Integer Programs},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Runtime Verification and Model Checking
Tue, Mar 19, 16:00 - 18:00, Room B1 (Chair: Natasha Sharygina)
Runtime Verification Based on Register Automata
Nikos Tzevelekos
(Queen Mary, University of London, UK; Microsoft Research, UK)
@InProceedings{ETAPS13p73,
author = {Nikos Tzevelekos},
title = {Runtime Verification Based on Register Automata},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
eVolCheck: Incremental Upgrade Checker for C
Natasha Sharygina
(University of Lugano, Switzerland)
@InProceedings{ETAPS13p81,
author = {Natasha Sharygina},
title = {eVolCheck: Incremental Upgrade Checker for C},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Concurrency and Learning & Abduction
Wed, Mar 20, 10:30 - 12:30, Room B1 (Chair: Corina Pasareanu)
Synthesis of Circular Compositional Program Proofs via Abduction
Mooly Sagiv
(College of William & Mary, USA; Microsoft Research, USA; Tel Aviv University, Israel)
@InProceedings{ETAPS13p89,
author = {Mooly Sagiv},
title = {Synthesis of Circular Compositional Program Proofs via Abduction},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Timed Automata
Wed, Mar 20, 15:00 - 16:00, Room B1 (Chair: Kim Larsen)
As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty
Oded Maler
(VERIMAG, France; Verimag/CNRS, France; CNRS-VERIMAG, France)
@InProceedings{ETAPS13p105,
author = {Oded Maler},
title = {As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Integer Parameter Synthesis for Timed Automata
Olivier H. Roux
(Ecole Centrale de Nantes, France; IRCCyN; IRCCyN/Ecole Centrale de Nantes, France)
@InProceedings{ETAPS13p109,
author = {Olivier H. Roux},
title = {Integer Parameter Synthesis for Timed Automata},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Security and Access Control
Wed, Mar 20, 16:30 - 18:00, Room B1 (Chair: Catuscia Palamidessi)
LTL Model-Checking for Malware Detection
Tayssir Touili
(LIAFA, CNRS & University Paris Diderot, France)
@InProceedings{ETAPS13p113,
author = {Tayssir Touili},
title = {LTL Model-Checking for Malware Detection},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Policy Analysis for Self-Administrated Role-Based Access Control
Gennaro Parlato
(University of Bristol, UK; University of Illinois, USA; University of Southampton, UK)
@InProceedings{ETAPS13p117,
author = {Gennaro Parlato},
title = {Policy Analysis for Self-Administrated Role-Based Access Control},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Frontiers and Functional Programs & Types
Thu, Mar 21, 10:30 - 12:30, Room B1 (Chair: Nir Piterman)
Automatic Testing of Real-Time Graphic Systems
Aram Timofeitchik
(Dfind Redpatch, Sweden; Chalmers | University of Gothenburg|, Sweden; DQ Consulting AB, Sweden)
@InProceedings{ETAPS13p125,
author = {Aram Timofeitchik},
title = {Automatic Testing of Real-Time Graphic Systems},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Equivalence Checking Quantum Protocols
Rajagopal Nagarajan
(University of Warwick, UK; University of Glasgow, UK; Middlesex University, UK)
@InProceedings{ETAPS13p129,
author = {Rajagopal Nagarajan},
title = {Equivalence Checking Quantum Protocols},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Encoding Monomorphic and Polymorphic Types
Nicholas Smallbone
(TU Muenchen, Germany; Technische Universität München, Germany; Chalmers University of Technology, Sweden)
@InProceedings{ETAPS13p133,
author = {Nicholas Smallbone},
title = {Encoding Monomorphic and Polymorphic Types},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Deriving Probability Density Functions from Probabilistic Functional Programs
Claudio Russo
(Georgia Institute of Technology, USA; Uppsala University, Sweden; Microsoft Research and University of Edinburgh, UK; Microsoft Research, UK)
@InProceedings{ETAPS13p137,
author = {Claudio Russo},
title = {Deriving Probability Density Functions from Probabilistic Functional Programs},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Tool Demos
Thu, Mar 21, 15:00 - 16:00, Room B1 (Chair: Laurie Hendren)
Polyglot: Systematic Analysis for Multiple Statechart Formalisms
Michael Lowry
(CMU, USA; Vanderbilt University, USA; NASA Ames Research Center, USA)
@InProceedings{ETAPS13p141,
author = {Michael Lowry},
title = {Polyglot: Systematic Analysis for Multiple Statechart Formalisms},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Memorax: Fence Inference under the TSO Memory Model
Ahmed Rezine
(Uppsala University, Sweden; Academia Sinica, Taiwan; Linköping University, Sweden)
@InProceedings{ETAPS13p145,
author = {Ahmed Rezine},
title = {Memorax: Fence Inference under the TSO Memory Model},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
AppGuard - Enforcing User Requirements on Android Apps
Philipp von Styp-Rekowsky
(Saarland University and Max Planck Institute for Software Systems, Germany; Saarland University, Germany)
@InProceedings{ETAPS13p153,
author = {Philipp von Styp-Rekowsky},
title = {AppGuard - Enforcing User Requirements on Android Apps},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Explicit State Model Checking and Büchi Automata
Thu, Mar 21, 16:30 - 18:00, Room B1 (Chair: Andrey Rybalchenko)
Model Checking Database Applications
Rupak Majumdar
(University of Illinois at Urbana-Champaign, USA; Max Planck Institute for Software Systems, Germany)
@InProceedings{ETAPS13p157,
author = {Rupak Majumdar},
title = {Model Checking Database Applications},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Efficient Property Preservation Checking of Model Refinements
Luc Engelen
(Eindhoven University of Technology, Netherlands)
@InProceedings{ETAPS13p161,
author = {Luc Engelen},
title = {Efficient Property Preservation Checking of Model Refinements},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
2nd Competition on Software Verification (SV-COMP)
Thu, Mar 21, 10:30 - 12:30, Room A1 (Chair: Dirk Beyer)
Second Competition on Software Verification
Dirk Beyer
(University of Passau, Germany)
@InProceedings{ETAPS13p169,
author = {Dirk Beyer},
title = {Second Competition on Software Verification},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
CSeq: A Sequentialization Tool for C (Competition Contribution)
Bernd Fischer
and Gennaro Parlato
(University of Southampton, UK)
@InProceedings{ETAPS13p181,
author = {Bernd Fischer and Gennaro Parlato},
title = {CSeq: A Sequentialization Tool for C (Competition Contribution)},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Handling Unbounded Loops with ESBMC 1.20 (Competition Contribution)
Jeremy Morse
and Bernd Fischer
(University of Southampton, UK; Universidade Federal do Amazonas, Brazil)
@InProceedings{ETAPS13p185,
author = {Jeremy Morse and Bernd Fischer},
title = {Handling Unbounded Loops with ESBMC 1.20 (Competition Contribution)},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
LLBMC: Improved Bounded Model Checking of C Programs Using LLVM
Stephan Falke
and Carsten Sinz
(Karlsruhe Institute of Technology (KIT), Germany)
@InProceedings{ETAPS13p189,
author = {Stephan Falke and Carsten Sinz},
title = {LLBMC: Improved Bounded Model Checking of C Programs Using LLVM},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Predator: A Tool for Verification of Low-level List Manipulation
Kamil Dudka
and Tomas Vojnar
(Brno University of Technology, Czech Republic)
@InProceedings{ETAPS13p193,
author = {Kamil Dudka and Tomas Vojnar},
title = {Predator: A Tool for Verification of Low-level List Manipulation},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution
Jiri Slaby
and Marek Trtík
(Faculty of Informatics, Masaryk University, Brno, Czech Republic; Masaryk University, Brno, Czech Republic)
@InProceedings{ETAPS13p197,
author = {Jiri Slaby and Marek Trtík},
title = {Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Threader: A Verifier for Multi-threaded Programs (Competition Contribution)
Corneliu Popeea
and Andrey Rybalchenko
(Technical University Munich, Germany; TUM, Germany)
@InProceedings{ETAPS13p201,
author = {Corneliu Popeea and Andrey Rybalchenko},
title = {Threader: A Verifier for Multi-threaded Programs (Competition Contribution)},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
UFO: Verification with Interpolants and Abstract Interpretation
Aws Albarghouthi
and Marsha Chechik
(University of Toronto, Canada; Software Engineering Institute, Carnegie Mellon University, USA)
@InProceedings{ETAPS13p205,
author = {Aws Albarghouthi and Marsha Chechik},
title = {UFO: Verification with Interpolants and Abstract Interpretation},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Ultimate Automizer with SMTInterpol
Matthias Heizmann
and Andreas Podelski
(University of Freiburg, Germany)
@InProceedings{ETAPS13p209,
author = {Matthias Heizmann and Andreas Podelski},
title = {Ultimate Automizer with SMTInterpol},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
Predicate Analysis with BLAST 2.7.1
Pavel Shved
and Vadim Mutilin
(ISPRAS, Russia)
@InProceedings{ETAPS13p213,
author = {Pavel Shved and Vadim Mutilin},
title = {Predicate Analysis with BLAST 2.7.1},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2013},
}
proc time: 0.26