![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
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
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
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.