Abstract is missing.
- Let this Graph Be Your Witness! - An Attestor for Verifying Java Pointer ProgramsHannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. 3-11 [doi]
- MaxSMT-Based Type Inference for Python 3Mostafa Hassan, Caterina Urban, Marco Eilers, Peter Müller 0001. 12-19 [doi]
- The JKind Model CheckerAndrew Gacek, John Backes, Mike Whalen, Lucas G. Wagner, Elaheh Ghassabani. 20-27 [doi]
- The DEEPSEC ProverVincent Cheval, Steve Kremer, Itsaka Rakotonirina. 28-36 [doi]
- SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate ReachabilityJianwen Li, Rohit Dureja, Geguang Pu, Kristin Yvonne Rozier, Moshe Y. Vardi. 37-44 [doi]
- StringFuzz: A Fuzzer for String SolversDmitry Blotsky, Federico Mora, Murphy Berzish, Yunhui Zheng, Ifaz Kabir, Vijay Ganesh. 45-51 [doi]
- Permission Inference for Array ProgramsJérôme Dohrau, Alexander J. Summers, Caterina Urban, Severin Münger, Peter Müller 0001. 55-74 [doi]
- Program Analysis Is Harder Than Verification: A Computability PerspectivePatrick Cousot, Roberto Giacobazzi, Francesco Ranzato. 75-95 [doi]
- Automata vs Linear-Programming Discounted-Sum InclusionSuguman Bansal, Swarat Chaudhuri, Moshe Y. Vardi. 99-116 [doi]
- Model Checking Indistinguishability of Randomized Security ProtocolsMatthew S. Bauer, Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan 0001. 117-135 [doi]
- Lazy Self-composition for Security VerificationWeikun Yang, Yakir Vizel, Pramod Subramanyan, Aarti Gupta, Sharad Malik. 136-156 [doi]
- SCInfer: Refinement-Based Verification of Software Countermeasures Against Side-Channel AttacksJun Zhang, Pengfei Gao, Fu Song, Chao Wang 0001. 157-177 [doi]
- Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness ObjectivesKrishnendu Chatterjee, Monika Henzinger, Veronika Loitzenbauer, Simin Oraee, Viktor Toman. 178-197 [doi]
- Attracting Tangles to Solve Parity GamesTom van Dijk. 198-215 [doi]
- Delta-Decision Procedures for Exists-Forall Problems over the RealsSoonho Kong, Armando Solar-Lezama, Sicun Gao. 219-235 [doi]
- Solving Quantified Bit-Vectors Using Invertibility ConditionsAina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli. 236-255 [doi]
- Understanding and Extending Incremental Determinization for 2QBFMarkus N. Rabe, Leander Tentrup, Cameron Rasmussen, Sanjit A. Seshia. 256-274 [doi]
- The Proof Complexity of SMT SolversRobert Robere, Antonina Kolokolova, Vijay Ganesh. 275-293 [doi]
- Model Generation for Quantified Formulas: A Taint-Based ApproachBenjamin Farinier, Sébastien Bardin, Richard Bonichon, Marie-Laure Potet. 294-313 [doi]
- Partial Order Aware Concurrency SamplingXinHao Yuan, Junfeng Yang, Ronghui Gu. 317-335 [doi]
- Reasoning About TSO Programs Using Reduction and AbstractionAhmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, Serdar Tasiran. 336-353 [doi]
- Quasi-Optimal Partial Order ReductionHuyen T. T. Nguyen, César Rodríguez, Marcelo Sousa, Camille Coti, Laure Petrucci. 354-371 [doi]
- On the Completeness of Verifying Message Passing Programs Under Bounded AsynchronyAhmed Bouajjani, Constantin Enea, Kailiang Ji, Shaz Qadeer. 372-391 [doi]
- Constrained Dynamic Partial Order ReductionElvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel, Albert Rubio. 392-410 [doi]
- Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging SystemMark Tullsen, Lee Pike, Nathan Collins, Aaron Tomb. 413-429 [doi]
- Continuous Formal Verification of Amazon s2nAndrey Chudnov, Nathan Collins, Byron Cook, Joey Dodds, Brian Huffman, Colm MacCárthaigh, Stephen Magill, Eric Mertens, Eric Mullen, Serdar Tasiran, Aaron Tomb, Eddy Westbrook. 430-446 [doi]
- Symbolic Liveness Analysis of Real-World SoftwareDaniel Schemmel, Julian Büning, Oscar Soria Dustmann, Thomas Noll, Klaus Wehrle. 447-466 [doi]
- Model Checking Boot Code from AWS Data CentersByron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle. 467-486 [doi]
- Android Stack MachineTaolue Chen, Jinlong He, Fu Song, Guozhen Wang, Zhilin Wu, Jun Yan. 487-504 [doi]
- Formally Verified Montgomery MultiplicationChristoph Walther. 505-522 [doi]
- Inner and Outer Approximating Flowpipes for Delay Differential EquationsEric Goubault, Sylvie Putot, Lorenz Sahlmann. 523-541 [doi]