DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories (English)
Free access
- New search for: Feng, Nick
- New search for: Hu, Alan J.
- New search for: Bayless, Sam
- New search for: Iqbal, Syed M.
- New search for: Trentin, Patrick
- New search for: Whalen, Mike
- New search for: Pike, Lee
- New search for: Backes, John
- New search for: Finkbeiner, Bernd
- New search for: Kovács, Laura
- New search for: Feng, Nick
- New search for: Hu, Alan J.
- New search for: Bayless, Sam
- New search for: Iqbal, Syed M.
- New search for: Trentin, Patrick
- New search for: Whalen, Mike
- New search for: Pike, Lee
- New search for: Backes, John
In:
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
;
Chapter: 1
;
3-23
;
2024
- Article/Chapter (Book) / Electronic Resource
-
Title:DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
-
Additional title:Lect.Notes Computer
-
Contributors:Finkbeiner, Bernd ( editor ) / Kovács, Laura ( editor ) / Feng, Nick ( author ) / Hu, Alan J. ( author ) / Bayless, Sam ( author ) / Iqbal, Syed M. ( author ) / Trentin, Patrick ( author ) / Whalen, Mike ( author ) / Pike, Lee ( author ) / Backes, John ( author )
-
Conference:International Conference on Tools and Algorithms for the Construction and Analysis of Systems ; 2024 ; Luxembourg City, Luxembourg
-
Published in: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 ; Chapter: 1 ; 3-23Lecture Notes in Computer Science ; 14570 ; 3-23
-
Publisher:
- New search for: Springer Nature Switzerland
-
Place of publication:Cham
-
Publication date:2024-04-04
-
Size:21 pages
-
ISBN:
-
ISSN:
-
DOI:
-
Type of media:Article/Chapter (Book)
-
Type of material:Electronic Resource
-
Language:English
-
Keywords:
-
Licence:
-
Source:
Table of contents eBook
The tables of contents are generated automatically and are based on the data records of the individual contributions available in the index of the TIB portal. The display of the Tables of Contents may therefore be incomplete.
- 1
-
DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic TheoriesFeng, Nick / Hu, Alan J. / Bayless, Sam / Iqbal, Syed M. / Trentin, Patrick / Whalen, Mike / Pike, Lee / Backes, John et al. | 2024
- 2
-
Z3-Noodler: An Automata-based String SolverChen, Yu-Fang / Chocholatý, David / Havlena, Vojtěch / Holík, Lukáš / Lengál, Ondřej / Síč, Juraj et al. | 2024
- 3
-
TaSSAT: Transfer and Share SATChowdhury, Md Solimul / Codel, Cayden R. / Heule, Marijn J. H. et al. | 2024
- 4
-
Speculative SAT Modulo SATHari Govind, V. K. / Garcia-Contreras, Isabel / Shoham, Sharon / Gurfinkel, Arie et al. | 2024
- 5
-
Happy Ending: An Empty Hexagon in Every Set of 30 PointsHeule, Marijn J. H. / Scheucher, Manfred et al. | 2024
- 6
-
Fully Generalized Reactivity(1) SynthesisEhlers, Rüdiger / Khalimov, Ayrat et al. | 2024
- 7
-
Knor: reactive synthesis using Oinkvan Dijk, Tom / van Abbema, Feije / Tomov, Naum et al. | 2024
- 8
-
On Dependent Variables in Reactive SynthesisAkshay, S. / Basa, Eliyahu / Chakraborty, Supratik / Fried, Dror et al. | 2024
- 9
-
CESAR: Control Envelope Synthesis via Angelic RefinementsKabra, Aditi / Laurent, Jonathan / Mitsch, Stefan / Platzer, André et al. | 2024
- 10
-
Answering Temporal Conjunctive Queries over Description Logic Ontologies for Situation Recognition in Complex Operational DomainsWesthofen, Lukas / Neurohr, Christian / Jung, Jean Christoph / Neider, Daniel et al. | 2024
- 11
-
Deciding Boolean Separation Logic via Small ModelsDacík, Tomáš / Rogalewicz, Adam / Vojnar, Tomáš / Zuleger, Florian et al. | 2024
- 12
-
Asynchronous Subtyping by Trace RelaxationBocchi, Laura / King, Andy / Murgia, Maurizio et al. | 2024
- 13
-
SootUp: A Redesign of the Soot Static Analysis FrameworkKarakaya, Kadiray / Schott, Stefan / Klauke, Jonas / Bodden, Eric / Schmidt, Markus / Luo, Linghui / He, Dongjie et al. | 2024
- 14
-
Formally verified asymptotic consensus in robust networksTekriwal, Mohit / Tachna-Fram, Avi / Jeannin, Jean-Baptiste / Kapritsos, Manos / Panagou, Dimitra et al. | 2024
- 15
-
Formally Verifying an Efficient SorterBeckert, Bernhard / Sanders, Peter / Ulbrich, Mattias / Wiesler, Julian / Witt, Sascha et al. | 2024
- 16
-
Explainable Online Monitoring of Metric First-Order Temporal LogicLima, Leonardo / Huerta y Munive, Jonathan Julián / Traytel, Dmitriy et al. | 2024
- 17
-
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOLLachnitt, Hanna / Fleury, Mathias / Aniva, Leni / Reynolds, Andrew / Barbosa, Haniel / Nötzli, Andres / Barrett, Clark / Tinelli, Cesare et al. | 2024
- 18
-
Automate where Automation Fails: Proof Strategies for Frama-C/WPCorrenson, Loïc / Blanchard, Allan / Djoudi, Adel / Kosmatov, Nikolai et al. | 2024
- 19
-
VeSCMul: Verified Implementation of S-C-Rewriting for Multiplier VerificationTemel, Mertcan et al. | 2024
- 20
-
A Logical Treatment of Finite AutomataRodrigues, Nishant / Sebe, Mircea Octavian / Chen, Xiaohong / Roşu, Grigore et al. | 2024
- 21
-
A State-of-the-Art Karp-Miller Algorithm Certified in CoqHilaire, Thibault / Ilcinkas, David / Leroux, Jérôme et al. | 2024