Abstract is missing.
- Verification, Testing, and Runtime Monitoring of Automotive Exhaust EmissionsHolger Hermanns, Sebastian Biewer, Pedro R. D'Argenio, Maximilian A. Köhl. 1-17 [doi]
- Playing with the Maximum-Flow ProblemOrna Kupferman. 18-25 [doi]
- Wayeb: a Tool for Complex Event ForecastingElias Alevizos, Alexander Artikis, Georgios Paliouras. 26-35 [doi]
- When Are Two Gossips the Same?Krzysztof R. Apt, Davide Grossi, Wiebe van der Hoek. 36-55 [doi]
- Function Summarization Modulo TheoriesSepideh Asadi, Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvärinen, Karine Even Mendoza, Natasha Sharygina, Hana Chockler. 56-75 [doi]
- Matching in the Description Logic FL0 with respect to General TBoxesFranz Baader, Oliver Fernandez Gil, Pavlos Marantidis. 76-94 [doi]
- Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel LogicMatthias Baaz, Anela Lolic. 95-110 [doi]
- Decidable Inequalities over Infinite TreesSabine Bauer, Steffen Jost, Martin Hofmann. 111-130 [doi]
- Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable SubsetsJaroslav Bendík, Ivana Cerna. 131-142 [doi]
- Why These Automata Types?Udi Boker. 143-163 [doi]
- A Verified Efficient Implementation of the LLL Basis Reduction AlgorithmRalph Bottesch, Max W. Haslbeck, René Thiemann. 164-180 [doi]
- Efficient SAT-Based Encodings of Conditional Cardinality ConstraintsAbdelhamid Boudane, Saïd Jabbour, Badran Raddaoui, Lakhdar Sais. 181-195 [doi]
- Reasoning About Prescription and Description Using Prioritized Default RulesValentin Cassano, Carlos Areces, Pablo Castro. 196-213 [doi]
- Two-variable First-Order Logic with Counting in ForestsWitold Charatonik, Yegor Guskov, Ian Pratt-Hartmann, Piotr Witkowski 0001. 214-232 [doi]
- Quasipolynomial Set-Based Symbolic Algorithms for Parity GamesKrishnendu Chatterjee, Wolfgang Dvorák, Monika Henzinger, Alexander Svozil. 233-253 [doi]
- The involutions-as-principal types/application-as-unification AnalogyAlberto Ciaffaglione, Furio Honsell, Marina Lenisa, Ivan Scagnetto. 254-270 [doi]
- Left-Handed Completeness for Kleene algebra, via Cyclic ProofsAnupam Das 0002, Amina Doumane, Damien Pous. 271-289 [doi]
- Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method AlgorithmGuillaume Davy, Eric Feron, Pierre-Loïc Garoche, Didier Henrion. 290-306 [doi]
- Graph Path OrderingsNachum Dershowitz, Jean-Pierre Jouannaud. 307-325 [doi]
- The Weak Completion Semantics and EqualityEmmanuelle-Anna Dietz, Steffen Hölldobler, Sibylle Schwarz, L. Yohanes Stefanus. 326-342 [doi]
- LTL with Arithmetic and its Applications in Reasoning about Hierarchical SystemsRachel Faran, Orna Kupferman. 343-362 [doi]
- Arrays Made Simpler: An Efficient, Scalable and Thorough PreprocessingBenjamin Farinier, Robin David, Sébastien Bardin, Matthieu Lemerre. 363-380 [doi]
- Loop Analysis by Quantification over IterationsBernhard Gleiss, Laura Kovács, Simon Robillard. 381-399 [doi]
- Formal verification of the YubiKey and YubiHSM APIs in Maude-NPAAntonio González-Burgueño, Damián Aparicio-Sánchez, Santiago Escobar, Catherine A. Meadows, José Meseguer. 400-417 [doi]
- Lookahead-Based SMT SolvingAntti E. J. Hyvärinen, Matteo Marescotti, Parvin Sadigova, Hana Chockler, Natasha Sharygina. 418-434 [doi]
- A Complete Cyclic Proof System for Inductive Entailments in First Order LogicRadu Iosif, Cristina Serban. 435-453 [doi]
- Towards Smarter MACE-style Model FindersMikolas Janota, Martin Suda. 454-470 [doi]
- Improving SAT-based Bounded Model Checking for Existential CTL through Path ReuseChuan Jiang, Gianfranco Ciardo. 471-487 [doi]
- Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Experimental Paper)Martin Jonás, Jan Strejcek. 488-497 [doi]
- Alternating Reachability Games with Behavioral and Revenue ObjectivesOrna Kupferman, Tami Tamir. 498-514 [doi]
- Polymorphic success types for ErlangFrancisco Javier López-Fraguas, Manuel Montenegro, Gorka Suárez-García. 515-533 [doi]
- SMTS: Distributed, Visualized Constraint SolvingMatteo Marescotti, Antti E. J. Hyvärinen, Natasha Sharygina. 534-542 [doi]
- Automatic Space Bound Analysis for Functional Programs with Garbage CollectionYue Niu, Jan Hoffmann. 543-563 [doi]
- A Verified Theorem Prover Backend Supported by a Monotonic LibraryVincent Rahli, Liron Cohen 0001, Mark Bickford. 564-582 [doi]
- A Theory of Satisfiability-Preserving Proofs in SAT SolvingAdrián Rebola-Pardo, Martin Suda. 583-603 [doi]
- The Triguarded Fragment of First-Order LogicSebastian Rudolph, Mantas Simkus. 604-619 [doi]
- Knowledge Compilation meets Uniform SamplingShubham Sharma, Rahul Gupta, Subhajit Roy, Kuldeep S. Meel. 620-636 [doi]
- Parse Condition: Symbolic Encoding of LL(1) ParsingDhruv Singal, Palak Agarwal, Saket Jhunjhunwala, Subhajit Roy. 637-655 [doi]
- Rewriting Environment for Arithmetic Circuit VerificationCunxi Yu, Atif Yasin, Tiankai Su, Alan Mishchenko, Maciej J. Ciesielski. 656-666 [doi]