


default search action
30th TACAS@ETAPS 2024: Luxembourg City, Luxembourg - Part I
- Bernd Finkbeiner
, Laura Kovács
:
Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I. Lecture Notes in Computer Science 14570, Springer 2024, ISBN 978-3-031-57245-6
SAT and SMT Solving
- Nick Feng, Alan J. Hu, Sam Bayless, Syed M. Iqbal, Patrick Trentin, Mike Whalen, Lee Pike, John Backes:
DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories. 3-23 - Yu-Fang Chen
, David Chocholatý
, Vojtech Havlena
, Lukás Holík
, Ondrej Lengál
, Juraj Síc
:
Z3-Noodler: An Automata-based String Solver. 24-33 - Md. Solimul Chowdhury
, Cayden R. Codel
, Marijn J. H. Heule
:
TaSSAT: Transfer and Share SAT. 34-42 - Hari Govind V. K.
, Isabel Garcia-Contreras
, Sharon Shoham
, Arie Gurfinkel
:
Speculative SAT Modulo SAT. 43-60 - Marijn J. H. Heule
, Manfred Scheucher
:
Happy Ending: An Empty Hexagon in Every Set of 30 Points. 61-80
Synthesis
- Rüdiger Ehlers, Ayrat Khalimov:
Fully Generalized Reactivity(1) Synthesis. 83-102 - Tom van Dijk
, Feije van Abbema, Naum Tomov:
Knor: reactive synthesis using Oink. 103-122 - S. Akshay, Eliyahu Basa, Supratik Chakraborty, Dror Fried:
On Dependent Variables in Reactive Synthesis. 123-143 - Aditi Kabra
, Jonathan Laurent
, Stefan Mitsch
, André Platzer
:
CESAR: Control Envelope Synthesis via Angelic Refinements. 144-164
Logic and Decidability
- Lukas Westhofen
, Christian Neurohr
, Jean Christoph Jung
, Daniel Neider
:
Answering Temporal Conjunctive Queries over Description Logic Ontologies for Situation Recognition in Complex Operational Domains. 167-187 - Tomás Dacík
, Adam Rogalewicz
, Tomás Vojnar
, Florian Zuleger
:
Deciding Boolean Separation Logic via Small Models. 188-206 - Laura Bocchi
, Andy King
, Maurizio Murgia
:
Asynchronous Subtyping by Trace Relaxation. 207-226
Program Analysis and Proofs
- Kadiray Karakaya, Stefan Schott, Jonas Klauke, Eric Bodden, Markus Schmidt, Linghui Luo
, Dongjie He:
SootUp: A Redesign of the Soot Static Analysis Framework. 229-247 - Mohit Tekriwal
, Avi Tachna-Fram, Jean-Baptiste Jeannin, Manos Kapritsos, Dimitra Panagou:
Formally verified asymptotic consensus in robust networks. 248-267 - Bernhard Beckert
, Peter Sanders
, Mattias Ulbrich
, Julian Wiesler, Sascha Witt
:
Formally Verifying an Efficient Sorter. 268-287 - Leonardo Lima
, Jonathan Julián Huerta y Munive
, Dmitriy Traytel
:
Explainable Online Monitoring of Metric First-Order Temporal Logic. 288-307
Proof Checking
- Hanna Lachnitt
, Mathias Fleury
, Leni Aniva
, Andrew Reynolds
, Haniel Barbosa
, Andres Nötzli
, Clark W. Barrett
, Cesare Tinelli
:
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. 311-330 - Loïc Correnson
, Allan Blanchard
, Adel Djoudi
, Nikolai Kosmatov
:
Automate where Automation Fails: Proof Strategies for Frama-C/WP. 331-339 - Mertcan Temel
:
VeSCMul: Verified Implementation of S-C-Rewriting for Multiplier Verification. 340-349 - Nishant Rodrigues
, Mircea Sebe, Xiaohong Chen
, Grigore Rosu
:
A Logical Treatment of Finite Automata. 350-369 - Thibault Hilaire
, David Ilcinkas
, Jérôme Leroux
:
A State-of-the-Art Karp-Miller Algorithm Certified in Coq. 370-389

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.