TACAS 2013

53 papers

1. A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems · Alexander Linden, Pierre Wolper
2. An Integrated Specification and Verification Technique for Highly Concurrent Data Structures · Parosh Aziz Abdulla, Frédéric Haziza, Lukás Holík, Bengt Jonsson, Ahmed Rezine
3. An Overview of the mCRL2 Toolset and Its Recent Advances · Sjoerd Cranen, Jan Friso Groote, Jeroen J. A. Keiren, Frank P. M. Stappers, Erik P. de Vink, Wieger Wesselink + 1 more
4. Analysis of Boolean Programs · Patrice Godefroid, Mihalis Yannakakis
5. AppGuard - Enforcing User Requirements on Android Apps · Michael Backes, Sebastian Gerling, Christian Hammer, Matteo Maffei, Philipp von Styp-Rekowsky
6. As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty · Jean-Francois Kempf, Marius Bozga, Oded Maler
7. Asynchronous Multi-core Incremental SAT Solving · Siert Wieringa, Keijo Heljanko
8. Automatic Testing of Real-Time Graphics Systems · Robert Nagy, Gerardo Schneider, Aram Timofeitchik
9. BULL: A Library for Learning Algorithms of Boolean Functions · Yu-Fang Chen, Bow-Yaw Wang
10. CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation - (Competition Contribution) · Stefan Löwe
11. CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis - (Competition Contribution) · Philipp Wendler
12. CSeq: A Sequentialization Tool for C - (Competition Contribution) · Bernd Fischer, Omar Inverso, Gennaro Parlato
13. Deriving Probability Density Functions from Probabilistic Functional Programs · Sooraj Bhat, Johannes Borgström, Andrew D. Gordon, Claudio V. Russo
14. Efficient Property Preservation Checking of Model Refinements · Anton Wijs, Luc Engelen
15. Encoding Monomorphic and Polymorphic Types · Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone
16. Equivalence Checking of Quantum Protocols · Ebrahim Ardeshir-Larijani, Simon J. Gay, Rajagopal Nagarajan
17. Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors · Ajith K. John, Supratik Chakraborty
18. Formula Preprocessing in MUS Extraction · Anton Belov, Matti Järvisalo, João Marques-Silva
19. Handling Unbounded Loops with ESBMC 1.20 - (Competition Contribution) · Jeremy Morse, Lucas C. Cordeiro, Denis A. Nicole, Bernd Fischer
20. Identifying Dynamic Data Structures by Learning Evolving Patterns in Memory · David H. White, Gerald Lüttgen
21. Integer Parameter Synthesis for Timed Automata · Aleksandra Jovanovic, Didier Lime, Olivier H. Roux
22. Intertwined Forward-Backward Reachability Analysis Using Interpolants · Yakir Vizel, Orna Grumberg, Sharon Shoham
23. LLBMC: Improved Bounded Model Checking of C Programs Using LLVM - (Competition Contribution) · Stephan Falke, Florian Merz, Carsten Sinz
24. LTL Model Checking of Interval Markov Chains · Michael Benedikt, Rastislav Lenhardt, James Worrell
25. LTL Model-Checking for Malware Detection · Fu Song, Tayssir Touili
26. Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO · Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, Ahmed Rezine
27. Model Checking Agent Knowledge in Dynamic Access Control Policies · Masoud Koleini, Eike Ritter, Mark Ryan
28. Model Checking Database Applications · Milos Gligoric, Rupak Majumdar
29. Model-Checking Iterated Games · Chung-Hao Huang, Sven Schewe, Farn Wang
30. On-the-Fly Exact Computation of Bisimilarity Distances · Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare
31. PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus · Radu Mateescu, Gwen Salaün
32. PRISM-games: A Model Checker for Stochastic Multi-Player Games · Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Aistis Simaitis
33. Policy Analysis for Self-administrated Role-Based Access Control · Anna Lisa Ferrara, P. Madhusudan, Gennaro Parlato
34. Polyglot: Systematic Analysis for Multiple Statechart Formalisms · Daniel Balasubramanian, Corina S. Pasareanu, Gabor Karsai, Michael R. Lowry
35. Predator: A Tool for Verification of Low-Level List Manipulation - (Competition Contribution) · Kamil Dudka, Petr Müller, Petr Peringer, Tomás Vojnar
36. Proof Tree Preserving Interpolation · Jürgen Christ, Jochen Hoenicke, Alexander Nutz
37. Ramsey vs. Lexicographic Termination Proving · Byron Cook, Abigail See, Florian Zuleger
38. Runtime Verification Based on Register Automata · Radu Grigore, Dino Distefano, Rasmus Lerchedahl Petersen, Nikos Tzevelekos
39. Second Competition on Software Verification - (Summary of SV-COMP 2013) · Dirk Beyer
40. Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking · Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud
41. Structural Counter Abstraction · Kshitij Bansal, Eric Koskinen, Thomas Wies, Damien Zufferey
42. Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution - (Competition Contribution) · Jiri Slaby, Jan Strejcek, Marek Trtík
43. Synthesis from LTL Specifications with Mean-Payoff Objectives · Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Jean-François Raskin
44. Synthesis of Circular Compositional Program Proofs via Abduction · Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Mooly Sagiv
45. The MathSAT5 SMT Solver · Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani
46. The Quest for Minimal Quotients for Probabilistic Automata · Christian Eisentraut, Holger Hermanns, Johann Schuster, Andrea Turrini, Lijun Zhang
47. Threader: A Verifier for Multi-threaded Programs - (Competition Contribution) · Corneliu Popeea, Andrey Rybalchenko
48. UFO: Verification with Interpolants and Abstract Interpretation - (Competition Contribution) · Aws Albarghouthi, Arie Gurfinkel, Yi Li, Sagar Chaki, Marsha Chechik
49. Ultimate Automizer with SMTInterpol - (Competition Contribution) · Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Evren Ermis, Jochen Hoenicke, Markus Lindenmann + 3 more
50. Unbounded Model-Checking with Interpolation for Regular Language Constraints · Graeme Gange, Jorge A. Navas, Peter J. Stuckey, Harald Søndergaard, Peter Schachte
51. Underapproximation of Procedure Summaries for Integer Programs · Pierre Ganty, Radu Iosif, Filip Konecný
52. Weighted Pushdown Systems with Indexed Weight Domains · Yasuhiko Minamide
53. eVolCheck: Incremental Upgrade Checker for C · Grigory Fedyukovich, Ondrej Sery, Natasha Sharygina