default search action
22nd TACAS 2016: Eindhoven, The Netherlands (Part of ETAPS 2016)
- Marsha Chechik, Jean-François Raskin
:
Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Lecture Notes in Computer Science 9636, Springer 2016, ISBN 978-3-662-49673-2
Unifying Talk
- Rupak Majumdar:
Robots at the Edge of the Cloud. 3-13
Abstraction and Verification I
- Alexey Bakhirkin, Nir Piterman
Finding Recurrent Sets with Backward Analysis and Trace Partitioning. 17-35 - Gudmund Grov, Vytautas Tumas:
Tactics for the Dafny Program Verifier. 36-53 - Caterina Urban, Arie Gurfinkel
Synthesizing Ranking Functions from Bits and Pieces. 54-70 - Radu Iosif, Adam Rogalewicz, Tomás Vojnar
Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems. 71-89
Probabilistic and Stochastic Systems I
- Luca Cardelli
Efficient Syntax-Driven Lumping of Differential Equations. 93-111 - Przemyslaw Daca, Thomas A. Henzinger, Jan Kretínský, Tatjana Petrov
Faster Statistical Model Checking for Unbounded Temporal Properties. 112-129 - Sebastian Junges, Nils Jansen
Safety-Constrained Reinforcement Learning for MDPs. 130-146 - Sadegh Esmaeil Zadeh Soudjani
Safety Verification of Continuous-Space Pure Jump Markov Processes. 147-163
Synthesis
- Christof Löding, P. Madhusudan, Daniel Neider
Abstract Learning Frameworks for Synthesis. 167-185 - Daniel Neider
Synthesizing Piece-Wise Functions by Learning Classifiers. 186-203 - Daniel Neider
An Automaton Learning Approach to Solving Safety Games over Infinite Graphs. 204-221
Probabilistic and Stochastic Systems II
- Olivier Bouissou, Eric Goubault, Sylvie Putot, Aleksandar Chakarov, Sriram Sankaranarayanan:
Uncertainty Propagation Using Probabilistic Affine Forms and Concentration of Measure Inequalities. 225-243 - Kim G. Larsen
Online and Compositional Learning of Controllers with Application to Floor Heating. 244-259 - Aleksandar Chakarov, Yuen-Lam Voronin, Sriram Sankaranarayanan:
Deductive Proofs of Almost Sure Persistence and Recurrence Properties. 260-279 - Rayna Dimitrova, Luis María Ferrer Fioriti, Holger Hermanns, Rupak Majumdar:
Probabilistic CTL*: The Deductive Way. 280-296
Tool Papers I
- Zhe Chen, Zhemin Wang, Yunlong Zhu, Hongwei Xi, Zhibin Yang:
Parametric Runtime Verification of C Programs. 299-315 - Alexander John Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink:
Coqoon - An IDE for Interactive Proof Development in Coq. 316-331 - Tom van Dijk
Multi-core Symbolic Bisimulation Minimisation. 332-348 - Joachim Klein
Advances in Symbolic Probabilistic Model Checking with PRISM. 349-366 - Milan Ceska
PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems. 367-384
Tool Papers II
- Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, Nir Piterman
T2: Temporal Property Verification. 387-393 - Souha Ben Rayana, Marius Bozga, Saddek Bensalem, Jacques Combaz:
RTD-Finder: A Tool for Compositional Verification of Real-Time Component-Based Systems. 394-406 - Martin Avanzini, Georg Moser, Michael Schaper:
TcT: Tyrolean Complexity Tool. 407-423 - Maria Christakis, K. Rustan M. Leino, Peter Müller, Valentin Wüstholz:
Integrated Environment for Diagnosing Verification Errors. 424-441 - Kasper Søe Luckow, Marko Dimjasevic, Dimitra Giannakopoulou, Falk Howar, Malte Isberner, Temesghen Kahsai, Zvonimir Rakamaric, Vishwanath Raman:
JDart: A Dynamic Symbolic Analysis Framework. 442-459
Concurrency
- Cédric Favre, Hagen Völzer, Peter Müller:
Diagnostic Information for Control-Flow Analysis of Workflow Graphs (a.k.a. Free-Choice Workflow Nets). 463-479 - Michael Blondin
Approaching the Coverability Problem Continuously. 480-496 - Constantin Enea, Azadeh Farzan:
On Atomicity in Presence of Non-atomic Writes. 497-514 - Daniel Poetzl, Daniel Kroening
Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models. 515-530
Tool Demos
- Benjamin Bittner, Marco Bozzano, Roberto Cavada, Alessandro Cimatti
The xSAP Safety Analysis Platform. 533-539 - Radu Calinescu, Kenneth Johnson
FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals. 540-546 - Sung-Shik T. Q. Jongmans, Farhad Arbab:
PrDK: Protocol Programming with Automata. 547-552 - Hugues Evrard:
DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation. 553-559 - Marta Kwiatkowska, David Parker
PRISM-Games 2.0: A Tool for Multi-objective Strategy Synthesis for Stochastic Games. 560-566 - Luca Compagna, Daniel Ricardo dos Santos
Cerberus: Automated Synthesis of Enforcement Mechanisms for Security-Sensitive Business Processes. 567-572 - Yuhui Lin, Pierre Le Bras
Developing and Debugging Proof Strategies by Tinkering. 573-579 - Rajdeep Mukherjee, Michael Tautschnig, Daniel Kroening
v2c - A Verilog to C Translator. 580-586
Abstraction and Verification II
- Kedar S. Namjoshi, Richard J. Trefler:
Parameterized Compositional Model Checking. 589-606 - Jan Friso Groote
An O(m\log n) Algorithm for Stuttering Equivalence and Branching Bisimulation. 607-624 - Sicun Gao, Damien Zufferey:
Interpolants in Nonlinear Theories Over the Reals. 625-641
Abstraction and Verification III
- Filip Konecný:
PTIME Computation of Transitive Closures of Octagonal Relations. 645-661 - Junkil Park, Miroslav Pajic, Insup Lee, Oleg Sokolsky:
Scalable Verification of Linear Controller Software. 662-679 - Pallavi Maiya, Rahul Gupta, Aditya Kanade, Rupak Majumdar:
Partial Order Reduction for Event-Driven Multi-threaded Programs. 680-697 - Mohamed Faouzi Atig, K. Narayan Kumar, Prakash Saivasan:
Acceleration in Multi-PushDown Systems. 698-714
Languages and Automata
- Ricardo Almeida
Reduction of Nondeterministic Tree Automata. 717-735 - Dogan Ulus
Online Timed Pattern Matching Using Derivatives. 736-751 - Nima Roohi, Pavithra Prabhakar, Mahesh Viswanathan:
Hybridization Based CEGAR for Hybrid Automata with Affine Dynamics. 752-769 - Frantisek Blahoudek
Complementing Semi-deterministic Büchi Automata. 770-787
Security
- Yongwang Zhao, David Sanán
Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication. 791-810 - Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich
Some Complexity Results for Stateful Network Verification. 811-830
Optimization
- Julien Lange
Characteristic Formulae for Session Types. 833-850 - Alexander Nadel
Bit-Vector Optimization. 851-867 - Normann Decker, Jannis Harder, Torben Scheffel, Malte Schmitz, Daniel Thoma:
Runtime Monitoring with Union-Find Structures. 868-884
Competition on Software Verification: SV-COMP
- Dirk Beyer
Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2016). 887-904 - Peter Schrammel
2LS for Program Analysis - (Competition Contribution). 905-907 - Manchun Zheng, John G. Edenhofner, Ziqing Luo, Mitchell J. Gerrard, Michael S. Rogers, Matthew B. Dwyer, Stephen F. Siegel:
CIVL: Applying a General Concurrency Verification Framework to C/Pthreads Programs (Competition Contribution). 908-911 - Karlheinz Friedberger
CPA-BAM: Block-Abstraction Memoization with Value Analysis and Predicate Analysis - (Competition Contribution). 912-915 - Stefan Löwe:
CPA-RefSel: CPAchecker with Refinement Selection - (Competition Contribution). 916-919 - Vladimír Still, Petr Rockai
DIVINE: Explicit-State LTL Model Checker - (Competition Contribution). 920-922 - Lukás Holík
Run Forester, Run Backwards! - (Competition Contribution). 923-926 - Olli Saarikivi
LCTD: Tests-Guided Proofs for C Programs on LLVM - (Competition Contribution). 927-929 - Egor George Karpenkov:
LPI: Software Verification with Local Policy Iteration - (Competition Contribution). 930-933 - Herbert O. Rocha
Hunting Memory Bugs in C Programs with Map2Check - (Competition Contribution). 934-937 - Ermenegildo Tomasco, Truc L. Nguyen, Omar Inverso
MU-CSeq 0.4: Individual Memory Location Unwindings - (Competition Contribution). 938-941 - Michal Kotoun, Petr Peringer, Veronika Soková, Tomás Vojnar
Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark - (Competition Contribution). 942-945 - Marek Chalupa
Symbiotic 3: New Slicer and Error-Witness Generation - (Competition Contribution). 946-949 - Matthias Heizmann
Ultimate Automizer with Two-track Proofs - (Competition Contribution). 950-953 - Henning Günther, Alfons Laarman
Vienna Verification Tool: IC3 for Parallel Software - (Competition Contribution). 954-957
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-14 20:48 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: