


default search action
24th TACAS 2018: Thessaloniki, Greece (Part of ETAPS 2018)
- Dirk Beyer, Marieke Huisman

:
Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I. Lecture Notes in Computer Science 10805, Springer 2018, ISBN 978-3-319-89959-6
Theorem Proving
- Giles Reger

, Martin Suda
, Andrei Voronkov:
Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning. 3-22 - Bohua Zhan:

Efficient Verification of Imperative Programs Using Auto2. 23-40 - Quang Loc Le

, Jun Sun
, Shengchao Qin
:
Frame Inference for Inductive Entailment Proofs in Separation Logic. 41-60 - Simon Wimmer

, Peter Lammich
:
Verified Model Checking of Timed Automata. 61-78
SAT and SMT I
- Randal E. Bryant

:
Chain Reduction for Binary and Zero-Suppressed Decision Diagrams. 81-98 - Hakan Metin, Souheib Baarir, Maximilien Colange, Fabrice Kordon:

CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving. 99-114 - Kshitij Bansal, Eric Koskinen, Omer Tripp:

Automatic Generation of Precise and Useful Commutativity Conditions. 115-132 - Seonmo Kim, Stephen McCamant:

Bit-Vector Model Counting Using Statistical Estimation. 133-151
Deductive Verification
- Maximilian P. L. Haslbeck

, Tobias Nipkow
:
Hoare Logics for Time Bounds - A Study in Meta Theory. 155-171 - Raphaël Cauderlier, Mihaela Sighireanu

:
A Verified Implementation of the Bounded List Container. 172-189 - Alexander J. Summers, Peter Müller

:
Automating Deductive Verification for Weak-Memory Programs. 190-209
Software Verification and Optimisation
- Shrawan Kumar

, Amitabha Sanyal, R. Venkatesh, Punit Shah:
Property Checking Array Programs Using Loop Shrinking. 213-231 - Daniel Neider

, Pranav Garg, P. Madhusudan, Shambwaditya Saha, Daejun Park:
Invariant Synthesis for Incomplete Verification Engines. 232-250 - Grigory Fedyukovich

, Rastislav Bodík:
Accelerating Syntax-Guided Invariant Synthesis. 251-269 - Eva Darulova

, Anastasiia Izycheva, Fariha Nasir, Fabian Ritter, Heiko Becker, Robert Bastian:
Daisy - Framework for Analysis and Optimization of Numerical Programs (Tool Paper). 270-287
Model Checking
- Tom van Dijk

:
Oink: An Implementation and Evaluation of Modern Parity Game Solvers. 291-308 - Rohit Dureja

, Kristin Yvonne Rozier
:
More Scalable LTL Model Checking via Discovering Design-Space Dependencies ( D^3 D 3 ). 309-327 - Chuan Jiang

, Gianfranco Ciardo
:
Generation of Minimum Tree-Like Witnesses for Existential CTL. 328-343 - Gabriele Costa

, David A. Basin, Chiara Bodei, Pierpaolo Degano, Letterio Galletta
:
From Natural Projection to Partial Model Checking and Back. 344-361
Machine Learning
- Adrien Champion, Tomoya Chiba, Naoki Kobayashi

, Ryosuke Sato
:
ICE-Based Refinement Type Discovery for Higher-Order Functional Programs. 365-384 - Tomás Brázdil, Krishnendu Chatterjee, Jan Kretínský

, Viktor Toman
:
Strategy Representation by Decision Trees in Reactive Synthesis. 385-407 - Matthew Wicker, Xiaowei Huang, Marta Kwiatkowska:

Feature-Guided Black-Box Safety Testing of Deep Neural Networks. 408-426

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.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














