Abstract is missing.
- Satisfiability Checking for Mission-Time LTLJianwen Li, Moshe Y. Vardi, Kristin Y. Rozier. 3-22 [doi]
- High-Level Abstractions for Simplifying Extended String Constraints in SMTAndrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli. 23-42 [doi]
- Alternating Automata Modulo First Order TheoriesRadu Iosif, Xiao Xu. 43-63 [doi]
- Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-VectorsMartin Jonás, Jan Strejcek. 64-73 [doi]
- cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided SynthesisAndrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli. 74-83 [doi]
- Incremental Determinization for Quantifier Elimination and Functional SynthesisMarkus N. Rabe. 84-94 [doi]
- Loop Summarization with Rational Vector Addition SystemsJake Silverman, Zachary Kincaid. 97-115 [doi]
- Invertibility Conditions for Floating-Point FormulasMartin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli. 116-136 [doi]
- Numerically-Robust Inductive Proof Rules for Continuous Dynamical SystemsSicun Gao, James Kapinski, Jyotirmoy V. Deshmukh, Nima Roohi, Armando Solar-Lezama, Nikos Arechiga, Soonho Kong. 137-154 [doi]
- Icing: Supporting Fast-Math Style Optimizations in a Verified CompilerHeiko Becker, Eva Darulova, Magnus O. Myreen, Zachary Tatlock. 155-173 [doi]
- Sound Approximation of Programs with Elementary FunctionsEva Darulova, Anastasia Volkova. 174-183 [doi]
- Formal Verification of Quantum Algorithms Using Quantum Hoare LogicJunyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, Naijun Zhan. 187-207 [doi]
- SecCSL: Security Concurrent Separation LogicGidon Ernst, Toby Murray. 208-230 [doi]
- Reachability Analysis for AWS-Based NetworksJohn Backes, Sam Bayless, Byron Cook, Catherine Dodge, Andrew Gacek, Alan J. Hu, Temesghen Kahsai, Bill Kocik, Evgenii Kotelnikov, Jure Kukovec, Sean McLaughlin, Jason Reed, Neha Rungta, John Sizemore, Mark A. Stalzer, Preethi Srinivasan, Pavle Subotic, Carsten Varming, Blake Whaley. 231-241 [doi]
- Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable LogicsIdan Berkovits, Marijana Lazic, Giuliano Losa, Oded Padon, Sharon Shoham. 245-266 [doi]
- Gradual Consistency CheckingRachid Zennou, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi. 267-285 [doi]
- Checking Robustness Against Snapshot IsolationSidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea. 286-304 [doi]
- Efficient Verification of Network Fault Tolerance via Counterexample-Guided RefinementNick Giannarakis, Ryan Beckett, Ratul Mahajan, David Walker. 305-323 [doi]
- On the Complexity of Checking Consistency for Replicated Data TypesRanadeep Biswas, Michael Emmi, Constantin Enea. 324-343 [doi]
- Communication-Closed Asynchronous ProtocolsAndrei Damian, Cezara Dragoi, Alexandru Militaru, Josef Widder. 344-363 [doi]
- Interpolating Strong InductionHari Govind Vediramana Krishnan, Yakir Vizel, Vijay Ganesh, Arie Gurfinkel. 367-385 [doi]
- Verifying Asynchronous Event-Driven Programs Using Partial Abstract TransformersPeizun Liu, Thomas Wahl, Akash Lal. 386-404 [doi]
- Inferring Inductive Invariants from Phase StructuresYotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv. 405-425 [doi]
- Termination of Triangular Integer Loops is DecidableFlorian Frohn, Jürgen Giesl. 426-444 [doi]
- AliveInLean: A Verified LLVM Peephole Optimization VerifierJuneyoung Lee, Chung-Kil Hur, Nuno P. Lopes. 445-455 [doi]
- Automated Parameterized Verification of CRDTsKartik Nagar, Suresh Jagannathan. 459-477 [doi]
- What's Wrong with On-the-Fly Partial Order ReductionStephen F. Siegel. 478-495 [doi]
- Integrating Formal Schedulability Analysis into a Verified OS KernelXiaojie Guo, Maxime Lesourd, Meng-qi Liu, Lionel Rieg, Zhong Shao. 496-514 [doi]
- Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOSYongwang Zhao, David Sanán. 515-533 [doi]
- Violat: Generating Tests of Observational Refinement for Concurrent ObjectsMichael Emmi, Constantin Enea. 534-546 [doi]