Abstract is missing.
- An O(m log n) algorithm for branching bisimilarity on labelled transition systemsDavid N. Jansen, Jan Friso Groote, Jeroen J. A. Keiren, Anton Wijs. 3-20 [doi]
- Verifying Quantum Communication Protocols with Ground BisimulationXudong Qin, Yuxin Deng, Wenjie Du. 21-38 [doi]
- Deciding the Bisimilarity of Context-Free Session TypesBernardo Almeida, Andreia Mordido, Vasco T. Vasconcelos. 39-56 [doi]
- Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong ModalitiesFrédéric Lang, Radu Mateescu 0001, Franco Mazzanti. 57-76 [doi]
- How Many Bits Does it Take to Quantize Your Neural Network?Mirco Giacobbe, Thomas A. Henzinger, Mathias Lechner. 79-97 [doi]
- Highly Automated Formal Proofs over Memory Usage of Assembly CodeFreek Verbeek, Joshua A. Bockenek, Binoy Ravindran. 98-117 [doi]
- GASOL: Gas Analysis and Optimization for Ethereum Smart ContractsElvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio. 118-125 [doi]
- CPU Energy Meter: A Tool for Energy-Aware Algorithms EngineeringDirk Beyer 0001, Philipp Wendler. 126-133 [doi]
- Practical Machine-Checked Formalization of Change Impact AnalysisKarl Palmskog, Ahmet Çelik, Milos Gligoric. 137-157 [doi]
- What's Decidable About Program Verification Modulo Axioms?Umang Mathur, P. Madhusudan, Mahesh Viswanathan 0001. 158-177 [doi]
- Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of RewritingAlexander Lochmann, Aart Middeldorp. 178-194 [doi]
- Fold/Unfold Transformations for Fixpoint LogicNaoki Kobayashi, Grigory Fedyukovich, Aarti Gupta. 195-214 [doi]
- Verifying OpenJDK's LinkedList using KeYHans-Dieter A. Hiep, Olaf Maathuis, Jinting Bian, Frank S. de Boer, Marko C. J. D. van Eekelen, Stijn de Gouw. 217-234 [doi]
- Analysing installation scenarios of Debian packagesBenedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen. 235-253 [doi]
- Endicheck: Dynamic Analysis for Detecting Endianness BugsRoman Kápl, Pavel Parízek. 254-270 [doi]
- Describing and Simulating Concurrent Quantum SystemsRichard Bornat, Jaap Boender, Florian Kammueller, Guillaume Poly, Rajagopal Nagarajan. 271-277 [doi]
- EMTST: Engineering the Meta-theory of Session TypesDavid Castro, Francisco Ferreira, Nobuko Yoshida. 278-285 [doi]
- Solving Mean-Payoff Games via Quasi DominionsMassimo Benerecetti, Daniele Dell'Erba, Fabio Mogavero. 289-306 [doi]
- Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation SystemsThomas Neele, Tim A. C. Willemse, Wieger Wesselink. 307-324 [doi]
- Polynomial Identification of ømega-AutomataDana Angluin, Dana Fisman, Yaara Shoval. 325-343 [doi]
- Advances in Automatic Software Verification: SV-COMP 2020Dirk Beyer. 347-367 [doi]
- 2LS: Heap Analysis and Memory Safety - (Competition Contribution)Viktor Malík, Peter Schrammel, Tomás Vojnar. 368-372 [doi]
- COASTAL: Combining Concolic and Fuzzing for Java (Competition Contribution)Willem Visser, Jaco Geldenhuys. 373-377 [doi]
- Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution)Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer 0001. 378-382 [doi]
- VeriAbs : Verification by Abstraction and Test Generation (Competition Contribution)Mohammad Afzal, Supratik Chakraborty, Avriti Chauhan, Bharti Chimdyalwar, Priyanka Darke, Ashutosh Gupta, Shrawan Kumar, Charles Babu M, Divyesh Unadkat, R. Venkatesh. 383-387 [doi]
- GACAL: Conjecture-Based Verification - (Competition Contribution)Benjamin Quiring, Panagiotis Manolios. 388-392 [doi]
- Java Ranger at SV-COMP 2020 (Competition Contribution)Vaibhav Sharma, Soha Hussein, Michael W. Whalen, Stephen McCamant, Willem Visser. 393-397 [doi]
- JDart: Dynamic Symbolic Execution for Java Bytecode (Competition Contribution)Malte Mues, Falk Howar. 398-402 [doi]
- Map2Check: Using Symbolic Execution and Fuzzing - (Competition Contribution)Herbert Rocha, Rafael Menezes, Lucas C. Cordeiro, Raimundo S. Barreto. 403-407 [doi]
- PredatorHP Revamped (Not Only) for Interval-Sized Memory Regions and Memory Reallocation (Competition Contribution)Petr Peringer, Veronika Soková, Tomás Vojnar. 408-412 [doi]
- Symbiotic 7: Integration of Predator and More - (Competition Contribution)Marek Chalupa, Tomás Jasek, Lukás Tomovic, Martin Hruska, Veronika Soková, Paulína Ayaziová, Jan Strejcek, Tomás Vojnar. 413-417 [doi]
- Ultimate Taipan with Symbolic Interpretation and Fluid Abstractions - (Competition Contribution)Daniel Dietsch, Matthias Heizmann, Alexander Nutz, Claus Schätzle, Frank Schüssele. 418-422 [doi]