Abstract is missing.
- The Spirit of Ghost CodeJean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich. 1-16 [doi]
- SMT-Based Model Checking for Recursive ProgramsAnvesh Komuravelli, Arie Gurfinkel, Sagar Chaki. 17-34 [doi]
- Property-Directed Shape AnalysisShachar Itzhaky, Nikolaj Bjørner, Thomas W. Reps, Mooly Sagiv, Aditya V. Thakur. 35-51 [doi]
- Shape Analysis via Second-Order Bi-AbductionQuang Loc Le, Cristian Gherghina, Shengchao Qin, Wei-Ngan Chin. 52-68 [doi]
- ICE: A Robust Framework for Learning InvariantsPranav Garg 0001, Christof Löding, P. Madhusudan, Daniel Neider. 69-87 [doi]
- From Invariant Checking to Invariant Inference Using Randomized SearchRahul Sharma 0001, Alex Aiken. 88-105 [doi]
- SMACK: Decoupling Source Language Details from Verifier ImplementationsZvonimir Rakamaric, Michael Emmi. 106-113 [doi]
- Synthesis of Masking Countermeasures against Side Channel AttacksHassan Eldib, Chao Wang. 114-130 [doi]
- Temporal Mode-Checking for Runtime Monitoring of Privacy PoliciesOmar Chowdhury, Limin Jia, Deepak Garg, Anupam Datta. 131-149 [doi]
- String Constraints for VerificationParosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman. 150-166 [doi]
- A Conference Management System with Verified Document ConfidentialitySudeep Kanav, Peter Lammich, Andrei Popescu 0001. 167-183 [doi]
- Vac - Verifier of Administrative Role-Based Access Control PoliciesAnna Lisa Ferrara, P. Madhusudan, Truc L. Nguyen, Gennaro Parlato. 184-191 [doi]
- From LTL to Deterministic Automata: A Safraless Compositional ApproachJavier Esparza, Jan Kretínský. 192-208 [doi]
- Symbolic Visibly Pushdown AutomataLoris D'Antoni, Rajeev Alur. 209-225 [doi]
- Engineering a Static Verification Tool for GPU KernelsEthel Bardsley, Adam Betts, Nathan Chong, Peter Collingbourne, Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema, Daniel Liew, Shaz Qadeer. 226-242 [doi]
- Lazy Annotation RevisitedKenneth L. McMillan. 243-259 [doi]
- Interpolating Property Directed ReachabilityYakir Vizel, Arie Gurfinkel. 260-276 [doi]
- Verifying Relative Error Bounds Using Symbolic SimulationJesse Bingham, Joe Leslie-Hurd. 277-292 [doi]
- Regression Test Selection for Distributed Software HistoriesMilos Gligoric, Rupak Majumdar, Rohan Sharma, Lamyaa Eloussi, Darko Marinov. 293-309 [doi]
- GPU-Based Graph Decomposition into Strongly Connected and Maximal End ComponentsAnton Wijs, Joost-Pieter Katoen, Dragan Bosnacki. 310-326 [doi]
- Software Verification in the Google App-Engine CloudDirk Beyer, Georg Dresler, Philipp Wendler. 327-333 [doi]
- The nuXmv Symbolic Model CheckerRoberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, Stefano Tonetta. 334-342 [doi]
- Analyzing and Synthesizing Genomic Logic FunctionsNicola Paoletti, Boyan Yordanov, Youssef Hamadi, Christoph M. Wintersteiger, Hillel Kugler. 343-357 [doi]
- Finding Instability in Biological ModelsByron Cook, Jasmin Fisher, Benjamin A. Hall, Samin Ishtiaq, Garvit Juniwal, Nir Piterman. 358-372 [doi]
- Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac CellsZhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra, Marta Z. Kwiatkowska. 373-390 [doi]
- Diamonds Are a Girl's Best Friend: Partial Order Reduction for Timed Automata with AbstractionsHenri Hansen, Shang-Wei Lin, Yang Liu, Truong Khanh Nguyen, Jun Sun 0001. 391-406 [doi]
- Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal ProjectionsWillem Hagemann. 407-423 [doi]
- Verifying LTL Properties of Hybrid Systems with K-LivenessAlessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta. 424-440 [doi]
- Safraless Synthesis for Epistemic Temporal SpecificationsRodica Bozianu, Catalin Dima, Emmanuel Filiot. 441-456 [doi]
- Minimizing Running Costs in Consumption SystemsTomás Brázdil, David Klaska, Antonín Kucera, Petr Novotný. 457-472 [doi]
- CEGAR for Qualitative Analysis of Probabilistic SystemsKrishnendu Chatterjee, Martin Chmelik, Przemyslaw Daca. 473-490 [doi]
- Optimal Guard Synthesis for Memory SafetyThomas Dillig, Isil Dillig, Swarat Chaudhuri. 491-507 [doi]
- Don't Sit on the Fence - A Static Analysis Approach to Automatic Fence InsertionJade Alglave, Daniel Kroening, Vincent Nimal, Daniel Poetzl. 508-524 [doi]
- MCMAS-SLK: A Model Checker for the Verification of Strategy Logic SpecificationsPetr Cermák, Alessio Lomuscio, Fabio Mogavero, Aniello Murano. 525-532 [doi]
- Solving Games without Controllable PredecessorNina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk, Adam Walker. 533-540 [doi]
- G4LTL-ST: Automatic Generation of PLC ProgramsChih-Hong Cheng, Chung-Hao Huang, Harald Ruess, Stefan Stattelmann. 541-549 [doi]
- Automatic Atomicity Verification for Clients of Concurrent Data StructuresMohsen Lesani, Todd D. Millstein, Jens Palsberg. 550-567 [doi]
- Regression-Free Synthesis for ConcurrencyPavol Cerný, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Thorsten Tarrach. 568-584 [doi]
- Bounded Model Checking of Multi-threaded C Programs via Lazy SequentializationOmar Inverso, Ermenegildo Tomasco, Bernd Fischer 0002, Salvatore La Torre, Gennaro Parlato. 585-602 [doi]
- An SMT-Based Approach to Coverability AnalysisJavier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp Meyer, Filip Niksic. 603-619 [doi]
- LEAP: A Tool for the Parametrized Verification of Concurrent DatatypesAlejandro Sánchez, César Sánchez. 620-627 [doi]
- Monadic DecompositionMargus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg. 628-645 [doi]
- A DPLL(T) Theory Solver for a Theory of Strings and Regular ExpressionsTianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, Morgan Deters. 646-662 [doi]
- Bit-Vector Rewriting with Automatic Rule GenerationAlexander Nadel. 663-679 [doi]
- A Tale of Two Solvers: Eager and Lazy Approaches to Bit-VectorsLiana Hadarean, Kshitij Bansal, Dejan Jovanovic, Clark Barrett, Cesare Tinelli. 680-695 [doi]
- AVATAR: The Architecture for First-Order Theorem ProversAndrei Voronkov. 696-710 [doi]
- Automating Separation Logic with Trees and DataRuzica Piskac, Thomas Wies, Damien Zufferey. 711-728 [doi]
- A Nonlinear Real Arithmetic FragmentAshish Tiwari, Patrick Lincoln. 729-736 [doi]
- Yices 2.2Bruno Dutertre. 737-744 [doi]
- A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity AnalysisMoritz Sinn, Florian Zuleger, Helmut Veith. 745-761 [doi]
- Symbolic Resource Bound Inference for Functional ProgramsRavichandhran Madhavan, Viktor Kuncak. 762-778 [doi]
- Proving Non-termination Using Max-SMTDaniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio. 779-796 [doi]
- Termination Analysis by Learning Terminating ProgramsMatthias Heizmann, Jochen Hoenicke, Andreas Podelski. 797-813 [doi]
- Causal Termination of Multi-threaded ProgramsAndrey Kupriyanov, Bernd Finkbeiner. 814-830 [doi]
- Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR)Johannes Birgmeier, Aaron R. Bradley, Georg Weissenbacher. 831-848 [doi]
- Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath AbstractionSuho Lee, Karem A. Sakallah. 849-865 [doi]
- QUICr: A Reusable Library for Parametric Abstraction of Sets and NumbersArlen Cox, Bor-Yuh Evan Chang, Sriram Sankaranarayanan. 866-873 [doi]