Abstract is missing.
- HAMPI: A String Solver for Testing, Analysis and Vulnerability DetectionVijay Ganesh, Adam Kiezun, Shay Artzi, Philip J. Guo, Pieter Hooimeijer, Michael D. Ernst. 1-19 [doi]
- Using Types for Software VerificationRanjit Jhala. 20 [doi]
- SMT-Based Modular Analysis of Sequential Systems CodeShuvendu K. Lahiri. 21-27 [doi]
- Logic and Compositional Verification of Hybrid Systems - (Invited Tutorial)André Platzer. 28-43 [doi]
- Using Coverage to Deploy Formal Verification in a Simulation WorldVigyan Singhal, Prashant Aggarwal. 44-49 [doi]
- Stability in Weak Memory ModelsJade Alglave, Luc Maranget. 50-66 [doi]
- Verification of Certifying ComputationsEyad Alkassar, Sascha Böhme, Kurt Mehlhorn, Christine Rizkallah. 67-82 [doi]
- Parameter Identification for Markov Models of Biochemical ReactionsAleksander Andreychenko, Linar Mikeev, David Spieler, Verena Wolf. 83-98 [doi]
- Getting Rid of Store-Buffers in TSO AnalysisMohamed Faouzi Atig, Ahmed Bouajjani, Gennaro Parlato. 99-115 [doi]
- Malware Analysis with Tree Automata InferenceDomagoj Babic, Daniel Reynaud, Dawn Song. 116-131 [doi]
- State/Event-Based LTL Model Checking under Parametric Generalized FairnessKyungmin Bae, José Meseguer. 132-148 [doi]
- Resolution Proofs and Skolem Functions in QBF Evaluation and ApplicationsValeriy Balabanov, Jie-Hong R. Jiang. 149-164 [doi]
- The BINCOA Framework for Binary Code AnalysisSébastien Bardin, Philippe Herrmann, Jérôme Leroux, Olivier Ly, Renaud Tabary, Aymeric Vincent. 165-170 [doi]
- CVC4Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, Cesare Tinelli. 171-177 [doi]
- SLAyer: Memory Safety for Systems-Level CodeJosh Berdine, Byron Cook, Samin Ishtiaq. 178-183 [doi]
- CPAchecker: A Tool for Configurable Software VerificationDirk Beyer, M. Erkan Keremoglu. 184-190 [doi]
- Existential Quantification as Incremental SATJörg Brauer, Andy King, Jael Kriener. 191-207 [doi]
- Efficient Analysis of Probabilistic Programs with an Unbounded CounterTomás Brázdil, Stefan Kiefer, Antonín Kucera. 208-224 [doi]
- Model Checking Algorithms for CTMDPsPeter Buchholz, Ernst Moritz Hahn, Holger Hermanns, Lijun Zhang. 225-242 [doi]
- Quantitative Synthesis for Concurrent ProgramsPavol Cerný, Krishnendu Chatterjee, Thomas A. Henzinger, Arjun Radhakrishna, Rohit Singh. 243-259 [doi]
- Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with Büchi ObjectivesKrishnendu Chatterjee, Monika Henzinger, Manas Joglekar, Nisarg Shah. 260-276 [doi]
- Smoothing a Program Soundly and RobustlySwarat Chaudhuri, Armando Solar-Lezama. 277-292 [doi]
- A Specialization Calculus for Pruning Disjunctive Predicates to Support VerificationWei-Ngan Chin, Cristian Gherghina, Razvan Voicu, Quang Loc Le, Florin Craciun, Shengchao Qin. 293-309 [doi]
- Kratos - A Software Model Checker for SystemCAlessandro Cimatti, Alberto Griggio, Andrea Micheli, Iman Narasamdya, Marco Roveri. 310-316 [doi]
- Efficient Scenario Verification for Hybrid AutomataAlessandro Cimatti, Sergio Mover, Stefano Tonetta. 317-332 [doi]
- Temporal Property Verification as a Program Analysis TaskByron Cook, Eric Koskinen, Moshe Y. Vardi. 333-348 [doi]
- Time for Statistical Model Checking of Real-Time SystemsAlexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, Zheng Wang. 349-355 [doi]
- Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent ProgramsAlastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Thomas Wahl. 356-371 [doi]
- Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation LogicKamil Dudka, Petr Peringer, Tomás Vojnar. 372-378 [doi]
- SpaceEx: Scalable Verification of Hybrid SystemsGoran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, Oded Maler. 379-395 [doi]
- From Cardiac Cells to Genetic Regulatory NetworksRadu Grosu, Grégory Batt, Flavio H. Fenton, James Glimm, Colas Le Guernic, Scott A. Smolka, Ezio Bartocci. 396-411 [doi]
- Threader: A Constraint-Based Verifier for Multi-threaded ProgramsAshutosh Gupta, Corneliu Popeea, Andrey Rybalchenko. 412-417 [doi]
- Interactive Synthesis of Code SnippetsTihomir Gvero, Viktor Kuncak, Ruzica Piskac. 418-423 [doi]
- Forest Automata for Verification of Heap ManipulationPeter Habermehl, Lukás Holík, Adam Rogalewicz, Jirí Simácek, Tomás Vojnar. 424-440 [doi]
- Synthesizing Cyber-Physical Architectural Models with Real-Time ConstraintsChristine Hang, Panagiotis Manolios, Vasilis Papavasileiou. 441-456 [doi]
- ::::μZ::::- An Efficient Engine for Fixed Points with ConstraintsKrystof Hoder, Nikolaj Bjørner, Leonardo Mendonça de Moura. 457-462 [doi]
- BAP: A Binary Analysis PlatformDavid Brumley, Ivan Jager, Thanassis Avgerinos, Edward J. Schwartz. 463-469 [doi]
- HMC: Verifying Functional Programs Using Abstract InterpretersRanjit Jhala, Rupak Majumdar, Andrey Rybalchenko. 470-485 [doi]
- A Quantifier Elimination Algorithm for Linear Modular Equations and DisequationsAjith K. John, Supratik Chakraborty. 486-503 [doi]
- Bug-Assist: Assisting Fault Localization in ANSI-C ProgramsManu Jose, Rupak Majumdar. 504-509 [doi]
- Synthesis of Distributed Control through Knowledge AccumulationGal Katz, Doron Peled, Sven Schewe. 510-525 [doi]
- Language Equivalence for Probabilistic AutomataStefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell. 526-540 [doi]
- Formalization and Automated Verification of RESTful BehaviorUri Klein, Kedar S. Namjoshi. 541-556 [doi]
- Linear Completeness Thresholds for Bounded Model CheckingDaniel Kroening, Joël Ouaknine, Ofer Strichman, Thomas Wahl, James Worrell. 557-572 [doi]
- Interpolation-Based Software Verification with WolverineDaniel Kroening, Georg Weissenbacher. 573-578 [doi]
- Synthesizing Biological TheoriesHillel Kugler, Cory Plock, Andy Roberts. 579-584 [doi]
- PRISM 4.0: Verification of Probabilistic Real-Time SystemsMarta Z. Kwiatkowska, Gethin Norman, David Parker. 585-591 [doi]
- Program Analysis for Overlaid Data StructuresOukseh Lee, Hongseok Yang, Rasmus Petersen. 592-608 [doi]
- KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ ProgramsGuodong Li, Indradeep Ghosh, Sreeranga P. Rajan. 609-615 [doi]
- Fully Symbolic Model Checking for Timed AutomataGeorges Morbé, Florian Pigorsch, Christoph Scholl. 616-632 [doi]
- Complete Formal Hardware Verification of Interfaces for a FlexRay-Like BusChristian Müller, Wolfgang Paul. 633-648 [doi]
- Synthia: Verification and Synthesis for Timed AutomataHans-Jörg Peter, Rüdiger Ehlers, Robert Mattmüller. 649-655 [doi]
- FixBag: A Fixpoint Calculator for Quantified Bag ConstraintsTuan-Hung Pham, Minh-Thai Trinh, Anh-Hoang Truong, Wei-Ngan Chin. 656-662 [doi]
- Analyzing Unsynthesizable Specifications for High-Level Robot Behavior Using LTLMoPVasumathi Raman, Hadas Kress-Gazit. 663-668 [doi]
- Practical, Low-Effort Equivalence Verification of Real CodeDavid A. Ramos, Dawson R. Engler. 669-685 [doi]
- Relational Abstractions for Continuous and Hybrid SystemsSriram Sankaranarayanan, Ashish Tiwari. 686-702 [doi]
- Simplifying Loop Invariant Generation Using Splitter PredicatesRahul Sharma 0001, Isil Dillig, Thomas Dillig, Alex Aiken. 703-719 [doi]
- Monitorability of Stochastic Dynamical SystemsA. Prasad Sistla, Milos Zefran, Yao Feng. 720-736 [doi]
- Equality-Based Translation Validator for LLVMMichael Stepp, Ross Tate, Sorin Lerner. 737-742 [doi]
- Model Checking Recursive Programs with Numeric Data TypesMatthew Hague, Anthony Widjaja Lin. 743-759 [doi]