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.