default search action
19th TACAS 2013: Rome, Italy (Part of ETAPS 2013)
- Nir Piterman, Scott A. Smolka:
Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. Lecture Notes in Computer Science 7795, Springer 2013, ISBN 978-3-642-36741-0
Markov Chains
- Giorgio Bacci
, Giovanni Bacci
On-the-Fly Exact Computation of Bisimilarity Distances. 1-15 - Christian Eisentraut, Holger Hermanns, Johann Schuster, Andrea Turrini, Lijun Zhang:
The Quest for Minimal Quotients for Probabilistic Automata. 16-31 - Michael Benedikt
LTL Model Checking of Interval Markov Chains. 32-46
Termination
- Byron Cook, Abigail See, Florian Zuleger:
Ramsey vs. Lexicographic Termination Proving. 47-61 - Kshitij Bansal, Eric Koskinen, Thomas Wies, Damien Zufferey:
Structural Counter Abstraction. 62-77
Quantifier Elimination
- Ajith K. John, Supratik Chakraborty
Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors. 78-92
SAT/SMT
- Alessandro Cimatti
The MathSAT5 SMT Solver. 93-107 - Anton Belov, Matti Järvisalo
Formula Preprocessing in MUS Extraction. 108-123 - Jürgen Christ, Jochen Hoenicke
Proof Tree Preserving Interpolation. 124-138 - Siert Wieringa, Keijo Heljanko
Asynchronous Multi-core Incremental SAT Solving. 139-153
Games and Synthesis
- Chung-Hao Huang, Sven Schewe
Model-Checking Iterated Games. 154-168 - Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Jean-François Raskin:
Synthesis from LTL Specifications with Mean-Payoff Objectives. 169-184 - Taolue Chen
PRISM-games: A Model Checker for Stochastic Multi-Player Games. 185-191
Process Algebra
- Radu Mateescu, Gwen Salaün:
PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus. 192-198 - Sjoerd Cranen, Jan Friso Groote
An Overview of the mCRL2 Toolset and Its Recent Advances. 199-213
Pushdown Systems Boolean/Integer Programs
- Patrice Godefroid, Mihalis Yannakakis:
Analysis of Boolean Programs. 214-229 - Yasuhiko Minamide:
Weighted Pushdown Systems with Indexed Weight Domains. 230-244 - Pierre Ganty, Radu Iosif, Filip Konecný:
Underapproximation of Procedure Summaries for Integer Programs. 245-259
Runtime Verification and Model Checking
- Radu Grigore, Dino Distefano, Rasmus Lerchedahl Petersen, Nikos Tzevelekos:
Runtime Verification Based on Register Automata. 260-276 - Graeme Gange
Unbounded Model-Checking with Interpolation for Regular Language Constraints. 277-291 - Grigory Fedyukovich
eVolCheck: Incremental Upgrade Checker for C. 292-307 - Yakir Vizel, Orna Grumberg, Sharon Shoham
Intertwined Forward-Backward Reachability Analysis Using Interpolants. 308-323
Concurrency
- Parosh Aziz Abdulla, Frédéric Haziza, Lukás Holík
An Integrated Specification and Verification Technique for Highly Concurrent Data Structures. 324-338 - Alexander Linden, Pierre Wolper
A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems. 339-353
Learning and Abduction
- David H. White, Gerald Lüttgen:
Identifying Dynamic Data Structures by Learning Evolving Patterns in Memory. 354-369 - Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Mooly Sagiv:
Synthesis of Circular Compositional Program Proofs via Abduction. 370-384
Timed Automata
- Jean-Francois Kempf, Marius Bozga, Oded Maler:
As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty. 385-400 - Aleksandra Jovanovic, Didier Lime
Integer Parameter Synthesis for Timed Automata. 401-415
Security and Access Control
- Fu Song, Tayssir Touili:
LTL Model-Checking for Malware Detection. 416-431 - Anna Lisa Ferrara, P. Madhusudan, Gennaro Parlato
Policy Analysis for Self-administrated Role-Based Access Control. 432-447 - Masoud Koleini, Eike Ritter, Mark Ryan
Model Checking Agent Knowledge in Dynamic Access Control Policies. 448-462
Frontiers (Graphics and Quantum)
- Robert Nagy, Gerardo Schneider, Aram Timofeitchik:
Automatic Testing of Real-Time Graphics Systems. 463-477 - Ebrahim Ardeshir-Larijani
Equivalence Checking of Quantum Protocols. 478-492
Functional Programs and Types
- Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone:
Encoding Monomorphic and Polymorphic Types. 493-507 - Sooraj Bhat, Johannes Borgström, Andrew D. Gordon, Claudio V. Russo:
Deriving Probability Density Functions from Probabilistic Functional Programs. 508-522
Tool Demonstrations
- Daniel Balasubramanian, Corina S. Pasareanu, Gabor Karsai
Polyglot: Systematic Analysis for Multiple Statechart Formalisms. 523-529 - Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen
Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO. 530-536 - Yu-Fang Chen
BULL: A Library for Learning Algorithms of Boolean Functions. 537-542 - Michael Backes, Sebastian Gerling, Christian Hammer
AppGuard - Enforcing User Requirements on Android Apps. 543-548
Explicit-State Model Checking
- Milos Gligoric, Rupak Majumdar:
Model Checking Database Applications. 549-564 - Anton Wijs
Efficient Property Preservation Checking of Model Refinements. 565-579
Büchi Automata
- Etienne Renault
Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking. 580-593
Competition on Software Verification
- Dirk Beyer
Second Competition on Software Verification - (Summary of SV-COMP 2013). 594-609 - Stefan Löwe:
CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation - (Competition Contribution). 610-612 - Philipp Wendler
CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis - (Competition Contribution). 613-615 - Bernd Fischer
CSeq: A Sequentialization Tool for C - (Competition Contribution). 616-618 - Jeremy Morse, Lucas C. Cordeiro
Handling Unbounded Loops with ESBMC 1.20 - (Competition Contribution). 619-622 - Stephan Falke, Florian Merz, Carsten Sinz:
LLBMC: Improved Bounded Model Checking of C Programs Using LLVM - (Competition Contribution). 623-626 - Kamil Dudka, Petr Müller, Petr Peringer, Tomás Vojnar
Predator: A Tool for Verification of Low-Level List Manipulation - (Competition Contribution). 627-629 - Jiri Slaby, Jan Strejcek, Marek Trtík:
Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution - (Competition Contribution). 630-632 - Corneliu Popeea, Andrey Rybalchenko:
Threader: A Verifier for Multi-threaded Programs - (Competition Contribution). 633-636 - Aws Albarghouthi, Arie Gurfinkel
UFO: Verification with Interpolants and Abstract Interpretation - (Competition Contribution). 637-640 - Matthias Heizmann
Ultimate Automizer with SMTInterpol - (Competition Contribution). 641-643
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-11-21 20:16 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: