Abstract is missing.
- Proving Absence of Starvation by Means of Abstract Interpretation and Model CheckingHelmut Seidl, Ralf Vogler. 3-22 [doi]
- Precise Null Pointer Analysis Through Global Value NumberingAnkush Das, Akash Lal. 25-41 [doi]
- May-Happen-in-Parallel Analysis with Returned FuturesElvira Albert, Samir Genaim, Pablo Gordillo. 42-58 [doi]
- JTDec: A Tool for Tree Decompositions in SootKrishnendu Chatterjee, Amir Kafshdar Goharshady, Andreas Pavlogiannis. 59-66 [doi]
- Fixing the State Budget: Approximation of Regular Languages with Small DFAsGraeme Gange, Pierre Ganty, Peter J. Stuckey. 67-83 [doi]
- An Equivalence Checking Framework for Array-Intensive ProgramsKunal Banerjee, Chittaranjan A. Mandal, Dipankar Sarkar. 84-90 [doi]
- Loop Quasi-Invariant Chunk DetectionJean-Yves Moyen, Thomas Rubiano, Thomas Seiller. 91-108 [doi]
- SamaTulyata: An Efficient Path Based Equivalence Checking ToolSoumyadip Bandyopadhyay, Santonu Sarkar, Dipankar Sarkar, Chittaranjan A. Mandal. 109-116 [doi]
- Tests and RefutationMohammad Torabi Dashti, David A. Basin. 119-138 [doi]
- The Density of Linear-Time PropertiesBernd Finkbeiner, Hazem Torfah. 139-155 [doi]
- HyLeak: Hybrid Analysis Tool for Information LeakageFabrizio Biondi, Yusuke Kawamoto 0001, Axel Legay, Louis-Marie Traonouez. 156-163 [doi]
- Compositional Safety Refutation TechniquesKumar Madhukar, Peter Schrammel, Mandayam K. Srivas. 164-183 [doi]
- Gradient-Based Variable Ordering of Decision Diagrams for Systems with Structural UnitsElvio Gilberto Amparore, Marco Beccuti, Susanna Donatelli. 184-200 [doi]
- Model Checking of C and C++ with DIVINE 4Zuzana Baranová, Jiri Barnat, Katarína Kejstová, Tadeás Kucera, Henrich Lauko, Jan Mrázek, Petr Rockai, Vladimír Still. 201-207 [doi]
- Dealing with Priorities and Locks for Concurrent ProgramsMarcio Diaz, Tayssir Touili. 208-224 [doi]
- Knowledge Transfer and Information Leakage in ProtocolsAbdullah Abdul Khadir, Madhavan Mukund, S. P. Suresh. 225-240 [doi]
- Concurrent Program Verification with Invariant-Guided UnderapproximationSumanth Prabhu, Peter Schrammel, Mandayam K. Srivas, Michael Tautschnig, Anand Yeolekar. 241-248 [doi]
- Maximum Resilience of Artificial Neural NetworksChih-Hong Cheng, Georg Nührenberg, Harald Ruess. 251-268 [doi]
- Formal Verification of Piece-Wise Linear Feed-Forward Neural NetworksRüdiger Ehlers. 269-286 [doi]
- Liquid Types for Array Invariant SynthesisManuel Montenegro, Susana Nieva, Ricardo Peña, Clara Segura. 289-306 [doi]
- Lifting CDCL to Template-Based Abstract Domains for Program VerificationRajdeep Mukherjee, Peter Schrammel, Leopold Haller, Daniel Kroening, Tom Melham. 307-326 [doi]
- Synthesizing Invariants by Solving Solvable LoopsSteven de Oliveira, Saddek Bensalem, Virgile Prevosto. 327-343 [doi]
- Exploiting Partial Knowledge for Efficient Model AnalysisNuno Macedo, Alcino Cunha, Eduardo Pessoa. 344-362 [doi]
- A Language-Theoretic View on Network ProtocolsPierre Ganty, Boris Köpf, Pedro Valero. 363-379 [doi]
- Efficient Strategy Iteration for Mean Payoff in Markov Decision ProcessesJan Kretínský, Tobias Meggendorfer. 380-399 [doi]
- Finding Polynomial Loop Invariants for Probabilistic ProgramsYijun Feng, Lijun Zhang 0001, David N. Jansen, Naijun Zhan, Bican Xia. 400-416 [doi]
- Synthesis of Optimal Resilient Control StrategiesChristel Baier, Clemens Dubslaff, Lubos Korenciak, Antonín Kucera, Vojtech Rehák. 417-434 [doi]
- ForFET: A Formal Feature Evaluation Tool for Hybrid SystemsAntonio Anastasio Bruto da Costa, Pallab Dasgupta. 437-445 [doi]
- Attacking the V: On the Resiliency of Adaptive-Horizon MPCAshish Tiwari, Scott A. Smolka, Lukas Esterle, Anna Lukina, Junxing Yang, Radu Grosu. 446-462 [doi]
- The Reach-Avoid Problem for Constant-Rate Multi-mode SystemsShankara Narayanan Krishna, Aviral Kumar, Fabio Somenzi, Behrouz Touri, Ashutosh Trivedi. 463-479 [doi]