Abstract is missing.
- Policy Monitoring in First-Order Temporal LogicDavid A. Basin, Felix Klaedtke, Samuel Müller. 1-18 [doi]
- Retrofitting Legacy Code for SecuritySomesh Jha. 19 [doi]
- Quantitative Information Flow: From Theory to Practice?Pasquale Malacaria. 20-22 [doi]
- Memory Management in Concurrent AlgorithmsMaged M. Michael. 23 [doi]
- ABC: An Academic Industrial-Strength Verification ToolRobert K. Brayton, Alan Mishchenko. 24-40 [doi]
- There s Plenty of Room at the Bottom: Analyzing and Verifying Machine CodeThomas W. Reps, Junghee Lim, Aditya V. Thakur, Gogul Balakrishnan, Akash Lal. 41-56 [doi]
- Constraint Solving for Program Verification: Theory and Practice by ExampleAndrey Rybalchenko. 57-71 [doi]
- Invariant Synthesis for Programs Manipulating Lists with Unbounded DataAhmed Bouajjani, Cezara Dragoi, Constantin Enea, Ahmed Rezine, Mihaela Sighireanu. 72-88 [doi]
- Termination Analysis with Compositional Transition InvariantsDaniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, Christoph M. Wintersteiger. 89-103 [doi]
- Lazy Annotation for Program Testing and VerificationKenneth L. McMillan. 104-118 [doi]
- The Static Driver Verifier Research PlatformThomas Ball, Ella Bounimova, Vladimir Levin, Rahul Kumar, Jakob Lichtenberg. 119-122 [doi]
- Dsolve: Safety Verification via Liquid TypesMing Kawaguchi, Patrick Maxim Rondon, Ranjit Jhala. 123-126 [doi]
- Contessa: Concurrency Testing Augmented with Symbolic AnalysisSudipta Kundu, Malay K. Ganai, Chao Wang. 127-131 [doi]
- Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion TestingParosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukás Holík, Chih-Duo Hong, Richard Mayr, Tomás Vojnar. 132-147 [doi]
- Efficient Emptiness Check for Timed Büchi AutomataFrédéric Herbreteau, B. Srivathsan, Igor Walukiewicz. 148-161 [doi]
- Merit: An Interpolating Model-CheckerNicolas Caniart. 162-166 [doi]
- Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid SystemsAlexandre Donzé. 167-170 [doi]
- Jtlv: A Framework for Developing Verification AlgorithmsAmir Pnueli, Yaniv Sa ar, Lenore D. Zuck. 171-174 [doi]
- Petruchio: From Dynamic Networks to NetsRoland Meyer, Tim Strazny. 175-179 [doi]
- Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid SystemsFederico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci. 180-195 [doi]
- Safety Verification for Probabilistic Hybrid SystemsLijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns, Ernst Moritz Hahn. 196-211 [doi]
- A Logical Product Approach to Zonotope IntersectionKhalil Ghorbal, Eric Goubault, Sylvie Putot. 212-226 [doi]
- Fast Acceleration of Ultimately Periodic RelationsMarius Bozga, Radu Iosif, Filip Konecný. 227-242 [doi]
- An Abstraction-Refinement Approach to Verification of Artificial Neural NetworksLuca Pulina, Armando Tacchella. 243-257 [doi]
- Fences in Weak Memory ModelsJade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell. 258-272 [doi]
- Generating Litmus Tests for Contrasting Memory Consistency ModelsSela Mador-Haim, Rajeev Alur, Milo M. K. Martin. 273-287 [doi]
- Directed Proof Generation for Machine CodeAditya V. Thakur, Junghee Lim, Akash Lal, Amanda Burton, Evan Driscoll, Matt Elder, Tycho Andersen, Thomas W. Reps. 288-305 [doi]
- Verifying Low-Level Implementations of High-Level DatatypesChristopher L. Conway, Clark Barrett. 306-320 [doi]
- Automatic Generation of Inductive Invariants from High-Level Microarchitectural Models of Communication FabricsSatrajit Chatterjee, Michael Kishinevsky. 321-338 [doi]
- Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verificationJuncao Li, Fei Xie, Thomas Ball, Vladimir Levin. 339-353 [doi]
- LTSmin: Distributed and Symbolic ReachabilityStefan Blom, Jaco van de Pol, Michael Weber 0002. 354-359 [doi]
- libalf: The Automata Learning FrameworkBenedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker, Daniel Neider, David R. Piegdon. 360-364 [doi]
- Symbolic Bounded SynthesisRüdiger Ehlers. 365-379 [doi]
- Measuring and Synthesizing Systems in Probabilistic EnvironmentsKrishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Rohit Singh. 380-395 [doi]
- Achieving Distributed Control through Model CheckingSusanne Graf, Doron Peled, Sophie Quinton. 396-409 [doi]
- Robustness in the Presence of LivenessRoderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger, Barbara Jobstmann. 410-424 [doi]
- RATSY - A New Requirements Analysis Tool with SynthesisRoderick Bloem, Alessandro Cimatti, Karin Greimel, Georg Hofferek, Robert Könighofer, Marco Roveri, Viktor Schuppan, Richard Seeber. 425-429 [doi]
- Comfusy: A Tool for Complete Functional SynthesisViktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter. 430-433 [doi]
- Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent ProgramsVineet Kahlon, Chao Wang. 434-449 [doi]
- Automatically Proving LinearizabilityViktor Vafeiadis. 450-464 [doi]
- Model Checking of Linearizability of Concurrent List ImplementationsPavol Cerný, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri, Rajeev Alur. 465-479 [doi]
- Local Verification of Global Invariants in Concurrent ProgramsErnie Cohen, Michal Moskal, Wolfram Schulte, Stephan Tobies. 480-494 [doi]
- Abstract Analysis of Symbolic ExecutionsAws Albarghouthi, Arie Gurfinkel, Ou Wei, Marsha Chechik. 495-510 [doi]
- Automated Assume-Guarantee Reasoning through Implicit LearningYu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang. 511-526 [doi]
- Learning Component Interfaces with May and Must AbstractionsRishabh Singh, Dimitra Giannakopoulou, Corina S. Pasareanu. 527-542 [doi]
- A Dash of Fairness for Compositional ReasoningAriel Cohen 0002, Kedar S. Namjoshi, Yaniv Sa ar. 543-557 [doi]
- SPLIT: A Compositional LTL VerifierAriel Cohen 0002, Kedar S. Namjoshi, Yaniv Sa ar. 558-561 [doi]
- A Model Checker for AADLMarco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri, Ralf Wimmer. 562-565 [doi]
- PESSOA: A Tool for Embedded Controller SynthesisManuel Mazo, Anna Davitian, Paulo Tabuada. 566-569 [doi]
- On Array Theory of Bounded ElementsMin Zhou, Fei He, Bow-Yaw Wang, Ming Gu. 570-584 [doi]
- Quantifier Elimination by Lazy Model EnumerationDavid Monniaux. 585-599 [doi]
- Bounded UnderapproximationsPierre Ganty, Rupak Majumdar, Benjamin Monmege. 600-614 [doi]
- Global Reachability in Bounded Phase Multi-stack Pushdown SystemsAnil Seth. 615-628 [doi]
- Model-Checking Parameterized Concurrent Programs Using Linear InterfacesSalvatore La Torre, P. Madhusudan, Gennaro Parlato. 629-644 [doi]
- Dynamic Cutoff Detection in Parameterized Concurrent ProgramsAlexander Kaiser, Daniel Kroening, Thomas Wahl. 645-659 [doi]
- PARAM: A Model Checker for Parametric Markov ModelsErnst Moritz Hahn, Holger Hermanns, Björn Wachter, Lijun Zhang. 660-664 [doi]
- Gist: A Solver for Probabilistic GamesKrishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Arjun Radhakrishna. 665-669 [doi]
- A NuSMV Extension for Graded-CTL Model CheckingAlessandro Ferrante, Maurizio Memoli, Margherita Napoli, Mimmo Parente, Francesco Sorrentino 0002. 670-673 [doi]