Abstract is missing.
- HOLL: Program Synthesis for Higher Order Logic LockingGourav Takhar, Ramesh Karri, Christian Pilato, Subhajit Roy. 3-24 [doi]
- The Complexity of LTL Rational SynthesisOrna Kupferman, Noam Shenwald. 25-45 [doi]
- Synthesis of Compact Strategies for Coordination ProgramsKedar S. Namjoshi, Nisarg Patel. 46-63 [doi]
- ZDD Boolean SynthesisYi Lin, Lucas M. Tabajara, Moshe Y. Vardi. 64-83 [doi]
- Comparative Verification of the Digital Library of Mathematical Functions and Computer Algebra SystemsAndré Greiner-Petter, Howard S. Cohl, Abdou Youssef, Moritz Schubotz, Avi Trost, Rajen Dey, Akiko Aizawa, Bela Gipp. 87-105 [doi]
- Verifying Fortran Programs with CIVLWenhao Wu, Jan Hückelheim, Paul D. Hovland, Stephen F. Siegel. 106-124 [doi]
- NORMA: a tool for the analysis of Relay-based Railway Interlocking SystemsArturo Amendola, Anna Becchi, Roberto Cavada, Alessandro Cimatti, Andrea Ferrando, Lorenzo Pilati, Giuseppe Scaglione, Alberto Tacchella, Marco Zamboni. 125-142 [doi]
- Efficient Neural Network Analysis with Sum-of-InfeasibilitiesHaoze Wu 0001, Aleksandar Zeljic, Guy Katz, Clark W. Barrett. 143-163 [doi]
- Formal Verification of the Ethereum 2.0 Beacon ChainFranck Cassez, Joanne Fuller, Aditya Asgaonkar. 167-182 [doi]
- Fast and Reliable Formal Verification of Smart Contracts with the Move ProverDavid L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Meng Xu, Jingyi Emma Zhong. 183-200 [doi]
- A Max-SMT Superoptimizer for EVM handling Memory and StorageElvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Albert Rubio. 201-219 [doi]
- A New Approach for Active Automata Learning Based on ApartnessFrits W. Vaandrager, Bharat Garhewal, Jurriaan Rot, Thorsten Wißmann. 223-243 [doi]
- Learning Realtime One-Counter AutomataVéronique Bruyère, Guillermo A. Pérez 0001, Gaëtan Staquet. 244-262 [doi]
- Scalable Anytime Algorithms for Learning Fragments of Linear Temporal LogicRitam Raha, Rajarshi Roy 0002, Nathanaël Fijalkow, Daniel Neider. 263-280 [doi]
- Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic ProcessesLuca Bortolussi, Giuseppe Maria Gallo, Jan Kretínský, Laura Nenzi. 281-300 [doi]
- Inferring Interval-Valued Floating-Point PreconditionsJonas Krämer, Lionel Blatter, Eva Darulova, Mattias Ulbrich. 303-321 [doi]
- NeuReach: Learning Reachability Functions from SimulationsDawei Sun, Sayan Mitra. 322-337 [doi]
- Inferring Invariants with Quantifier Alternations: Taming the Search Space ExplosionJason R. Koenig, Oded Padon, Sharon Shoham, Alex Aiken. 338-356 [doi]
- LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation FunctionsBrandon Paulsen, Chao Wang 0001. 357-376 [doi]
- Kmclib: Automated Inference and Verification of Session Types from OCaml ProgramsKeigo Imai, Julien Lange, Rumyana Neykova. 379-386 [doi]
- Automated Translation of Natural Language Requirements to Runtime MonitorsIvan Perez 0003, Anastasia Mavridou, Thomas Pressburger, Alwyn Goodloe, Dimitra Giannakopoulou. 387-395 [doi]
- MaskD: A Tool for Measuring Masking Fault-ToleranceLuciano Putruele, Ramiro Demasi, Pablo F. Castro, Pedro R. D'Argenio. 396-403 [doi]
- Better Counterexamples for DafnyAleksandar Chakarov, Aleksandr Fedchin, Zvonimir Rakamaric, Neha Rungta. 404-411 [doi]
- cvc5: A Versatile and Industrial-Strength SMT SolverHaniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds 0001, Ying Sheng 0007, Cesare Tinelli, Yoni Zohar. 415-442 [doi]
- Clausal Proofs for Pseudo-Boolean ReasoningRandal E. Bryant, Armin Biere, Marijn J. H. Heule. 443-461 [doi]
- Moving Definition Variables in Quantified Boolean FormulasJoseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant. 462-479 [doi]
- A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear ArithmeticMartin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Larry González, Markus Krötzsch, Maximilian Marx 0001, Harish K. Murali, Christoph Weidenbach. 480-501 [doi]
- Property Directed Reachability for Generalized Petri NetsNicolas Amat, Silvano Dal-Zilio, Thomas Hujsa. 505-523 [doi]
- Transition Power Abstractions for Deep Counterexample DetectionMartin Blicha, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina. 524-542 [doi]
- Searching for Ribbon-Shaped Paths in Fair Transition SystemsMarco Bozzano, Alessandro Cimatti, Stefano Tonetta, Viktória Vozárová. 543-560 [doi]
- CoVeriTeam: On-Demand Composition of Cooperative Verification SystemsDirk Beyer 0001, Sudeep Kanav. 561-579 [doi]