default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID20th TACAS 2014: Grenoble, France (Part of ETAPS 2014)
- Erika Ábrahám
, Klaus Havelund:
Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings. Lecture Notes in Computer Science 8413, Springer 2014, ISBN 978-3-642-54861-1
Invited Contribution
- Orna Kupferman:
Variations on Safety. 1-14
Decision Procedures and Their Application in Analysis
- Francesco Alberti, Silvio Ghilardi, Natasha Sharygina:
Decision Procedures for Flat Array Properties. 15-30 - Alessandro Armando, Roberto Carbone, Luca Compagna:
SATMC: A SAT-Based Model Checker for Security-Critical Systems. 31-45 - Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta:
IC3 Modulo Theories via Implicit Predicate Abstraction. 46-61 - Hassan Eldib, Chao Wang, Patrick Schaumont:
SMT-Based Verification of Software Countermeasures against Side-Channel Attacks. 62-77 - Bernd Finkbeiner, Leander Tentrup:
Detecting Unrealizable Specifications of Distributed Systems. 78-92 - Arie Gurfinkel, Anton Belov, João Marques-Silva:
Synthesizing Safe Bit-Precise Invariants. 93-108 - Michael Huth, Jim Huan-Pu Kuo:
PEALT: An Automated Reasoning Tool for Numerical Aggregation of Trust Evidence. 109-123 - Ruzica Piskac, Thomas Wies, Damien Zufferey:
GRASShopper - Complete Heap Verification with Mixed Specifications. 124-139
Complexity and Termination Analysis
- Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, Jürgen Giesl:
Alternating Runtime and Size Complexity Analysis of Integer Programs. 140-155 - Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn:
Proving Nontermination via Safety. 156-171 - Jan Leike, Matthias Heizmann:
Ranking Templates for Linear Loops. 172-186
Modeling and Model Checking Discrete Systems
- Thomas Gibson-Robinson, Philip J. Armstrong, Alexandre Boulgakov, A. W. Roscoe:
FDR3 - A Modern Refinement Checker for CSP. 187-201 - Gavin Lowe:
Concurrent Depth-First Search Algorithms. 202-216 - Jan Reineke, Stavros Tripakis:
Basic Problems in Multi-View Modeling. 217-232 - Anton Wijs, Dragan Bosnacki:
GPUexplore: Many-Core On-the-Fly State Space Exploration Using GPUs. 233-247
Timed and Hybrid Systems
- Dieky Adzkiya, Bart De Schutter, Alessandro Abate:
Forward Reachability Computation for Autonomous Max-Plus-Linear Systems. 248-262 - Lacramioara Astefanoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga, Jacques Combaz:
Compositional Invariant Generation for Timed Systems. 263-278 - Khalil Ghorbal, André Platzer:
Characterizing Algebraic Invariants by Differential Radical Invariants. 279-294 - Christian Herrera, Bernd Westphal, Andreas Podelski:
Quasi-Equal Clock Reduction: More Networks, More Queries. 295-309 - Ting Wang, Jun Sun, Yang Liu, Xinyu Wang, Shanping Li:
Are Timed Automata Bad for a Specification Language? Language Inclusion Checking for Timed Automata. 310-325
Monitoring, Fault Detection and Identification
- Marco Bozzano, Alessandro Cimatti, Marco Gario, Stefano Tonetta:
Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic. 326-340 - Normann Decker, Martin Leucker, Daniel Thoma:
Monitoring Modulo Theories. 341-356 - Thomas Reinbacher, Kristin Yvonne Rozier, Johann Schumann:
Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems. 357-372
Competition on Software Verification
- Dirk Beyer:
Status Report on Software Verification - (Competition Summary SV-COMP 2014). 373-388 - Daniel Kroening, Michael Tautschnig:
CBMC - C Bounded Model Checker - (Competition Contribution). 389-391 - Stefan Löwe, Mikhail U. Mandrykin, Philipp Wendler:
CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses - (Competition Contribution). 392-394 - Petr Müller, Tomás Vojnar:
CPAlien: Shape Analyzer for CPAChecker - (Competition Contribution). 395-397 - Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, Gennaro Parlato:
Lazy-CSeq: A Lazy Sequentialization Tool for C - (Competition Contribution). 398-401 - Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato:
MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings - (Competition Contribution). 402-404 - Jeremy Morse, Mikhail Ramalho, Lucas C. Cordeiro, Denis A. Nicole, Bernd Fischer:
ESBMC 1.22 - (Competition Contribution). 405-407 - Arie Gurfinkel, Anton Belov:
FrankenBit: Bit-Precise Verification with Many Bits - (Competition Contribution). 408-411 - Kamil Dudka, Petr Peringer, Tomás Vojnar:
Predator: A Shape Analyzer Based on Symbolic Memory Graphs - (Competition Contribution). 412-414 - Jiri Slaby, Jan Strejcek:
Symbiotic 2: More Precise Slicing - (Competition Contribution). 415-417 - Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Jochen Hoenicke, Markus Lindenmann, Betim Musa, Christian Schilling, Stefan Wissert, Andreas Podelski:
Ultimate Automizer with Unsatisfiable Cores - (Competition Contribution). 418-420 - Evren Ermis, Alexander Nutz, Daniel Dietsch, Jochen Hoenicke, Andreas Podelski:
Ultimate Kojak - (Competition Contribution). 421-423
Specifying and Checking Linear Time Properties
- Shaull Almagor, Udi Boker, Orna Kupferman:
Discounting in LTL. 424-439 - Ala-Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon, Yann Thierry-Mieg:
Symbolic Model Checking of Stutter-Invariant Properties Using Generalized Testing Automata. 440-454
Synthesis and Learning
- Xiaowei Huang, Ron van der Meyden:
Symbolic Synthesis for Epistemic Specifications with Observational Semantics. 455-469 - Wenchao Li, Dorsa Sadigh, S. Shankar Sastry, Sanjit A. Seshia:
Synthesis for Human-in-the-Loop Control Systems. 470-484 - Oded Maler, Irini-Eleftheria Mens:
Learning Regular Languages over Large Alphabets. 485-499
Quantum and Probabilistic Systems
- Ebrahim Ardeshir-Larijani, Simon J. Gay, Rajagopal Nagarajan:
Verification of Concurrent Quantum Protocols by Equivalence Checking. 500-514 - Christel Baier, Joachim Klein, Sascha Klüppelholz, Steffen Märcker:
Computing Conditional Probabilities in Markovian Models Efficiently. 515-530 - Klaus Dräger, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Mateusz Ujma:
Permissive Controller Synthesis for Probabilistic Systems. 531-546 - Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate:
Precise Approximations of the Probability Distribution of a Markov Process in Time: An Application to Probabilistic Invariance. 547-561
Tool Demonstrations
- Elvira Albert, Puri Arenas, Antonio Flores-Montoya, Samir Genaim, Miguel Gómez-Zamalloa, Enrique Martin-Martin, German Puebla, Guillermo Román-Díez:
SACO: Static Analyzer for Concurrent Objects. 562-567 - Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti:
VeriMAP: A Tool for Verifying Programs through Transformations. 568-574 - D. A. van Beek, Wan J. Fokkink, Dennis Hendriks, Albert T. Hofkamp, Jasen Markovski, Joanna M. van de Mortel-Fronczak, Michel A. Reniers:
CIF 3: Model-Based Engineering of Supervisory Controllers. 575-580 - Rafael Caballero, Enrique Martin-Martin, Adrián Riesco, Salvador Tamarit:
EDD: A Declarative Debugger for Sequential Erlang Programs. 581-586 - Vincent Cheval:
APTE: An Algorithm for Proving Trace Equivalence. 587-592 - Arnd Hartmanns, Holger Hermanns:
The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification. 593-598 - Antti Siirtola:
Bounds2: A Tool for Compositional Multi-parametrised Verification. 599-604
Case Studies
- Jaap Boender, Claudio Sacerdoti Coen:
On the Correctness of a Branch Displacement Algorithm. 605-619 - Christian von Essen, Dimitra Giannakopoulou:
Analyzing the Next Generation Airborne Collision Avoidance System. 620-635 - Erwan Jahier, Simplice Djoko Djoko, Chaouki Maiza, Eric Lafont:
Environment-Model Based Testing of Control Systems: Case Studies. 636-650
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 2025-11-29 00:04 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:
