Table of Contents

• THERE AND BACK AGAIN: Lessons Learned on the Way to the MarketRance Cleaveland. 1 [doi]
• Verifying Object-Oriented Software: Lessons and ChallengesK. Rustan M. Leino. 2 [doi]
• Shape Analysis by Graph DecompositionRoman Manevich, Josh Berdine, Byron Cook, Ganesan Ramalingam, Mooly Sagiv. 3-18 [doi]
• A Reachability Predicate for Analyzing Low-Level SoftwareShaunak Chatterjee, Shuvendu K. Lahiri, Shaz Qadeer, Zvonimir Rakamaric. 19-33 [doi]
• Generating Representation Invariants of Structurally Complex DataMuhammad Zubair Malik, Aman Pervaiz, Sarfraz Khurshid. 34-49 [doi]
• Multi-objective Model Checking of Markov Decision ProcessesKousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, Mihalis Yannakakis. 50-65 [doi]
• PReMo : An Analyzer for P robabilistic Re cursive Mo delsDominik Wojtczak, Kousha Etessami. 66-71 [doi]
• Counterexamples in Probabilistic Model CheckingTingting Han, Joost-Pieter Katoen. 72-86 [doi]
• Bisimulation Minimisation Mostly Speeds Up Probabilistic Model CheckingJoost-Pieter Katoen, Tim Kemna, Ivan S. Zapreev, David N. Jansen. 87-101 [doi]
• Causal Dataflow Analysis for Concurrent ProgramsAzadeh Farzan, P. Madhusudan. 102-116 [doi]
• Type-Dependence Analysis and Program Transformation for Symbolic ExecutionSaswat Anand, Alessandro Orso, Mary Jean Harrold. 117-133 [doi]
• JPF-SE: A Symbolic Execution Extension to Java PathFinderSaswat Anand, Corina S. Pasareanu, Willem Visser. 134-138 [doi]
• A Symbolic Algorithm for Optimal Markov Chain LumpingSalem Derisavi. 139-154 [doi]
• Flow Faster: Efficient Decision Algorithms for Probabilistic SimulationsLijun Zhang, Holger Hermanns, Friedrich Eisenbrand, David N. Jansen. 155-169 [doi]
• Model Checking Probabilistic Timed Automata with One or Two ClocksMarcin Jurdzinski, François Laroussinie, Jeremy Sproston. 170-184 [doi]
• Adaptor Synthesis for Real-Time ComponentsMassimo Tivoli, Pascal Fradet, Alain Girault, Gregor Gößler. 185-200 [doi]
• Deciding an Interval Logic with Accumulated DurationsMartin Fränzle, Michael R. Hansen. 201-215 [doi]
• From Time Petri Nets to Timed Automata: An Untimed ApproachDavide D Aprile, Susanna Donatelli, Arnaud Sangnier, Jeremy Sproston. 216-230 [doi]
• Complexity in Simplicity: Flexible Agent-Based State Space ExplorationJacob Illum Rasmussen, Gerd Behrmann, Kim Guldstrand Larsen. 231-245 [doi]
• On Sampling Abstraction of Continuous Time Logic with DurationsParitosh K. Pandya, Shankara Narayanan Krishna, Kuntal Loya. 246-260 [doi]
• Assume-Guarantee SynthesisKrishnendu Chatterjee, Thomas A. Henzinger. 261-275 [doi]
• Optimized L*-Based Assume-Guarantee ReasoningSagar Chaki, Ofer Strichman. 276-291 [doi]
• Refining Interface Alphabets for Compositional VerificationMihaela Gheorghiu, Dimitra Giannakopoulou, Corina S. Pasareanu. 292-307 [doi]
• MAVEN: Modular Aspect VerificationMax Goldman, Shmuel Katz. 308-322 [doi]
• Model Checking Liveness Properties of Genetic Regulatory NetworksGrégory Batt, Calin Belta, Ron Weiss. 323-338 [doi]
• Checking Pedigree Consistency with PCSPanagiotis Manolios, Marc Galceran Oms, Sergi Oliva Valls. 339-342 [doi]
• Don t Care Modeling: A Logical Framework for Developing Predictive System ModelsHillel Kugler, Amir Pnueli, Michael J. Stern, E. Jane Albert Hubbard. 343-357 [doi]
• Deciding Bit-Vector Arithmetic with AbstractionRandal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady. 358-372 [doi]
• Abstraction Refinement of Linear Programs with ArraysAlessandro Armando, Massimo Benerecetti, Jacopo Mantovani. 373-388 [doi]
• Property-Driven Partitioning for Abstraction RefinementRoberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi. 389-404 [doi]
• Combining Abstraction Refinement and SAT-Based Model CheckingNina Amla, Kenneth L. McMillan. 405-419 [doi]
• Detecting Races in Ensembles of Message Sequence ChartsEdith Elkind, Blaise Genest, Doron Peled. 420-434 [doi]
• Replaying Play In and Play Out: Synthesis of Design Models from Scenarios by LearningBenedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker. 435-450 [doi]
• Improved Algorithms for the Automata-Based Approach to Model-CheckingLaurent Doyen, Jean-François Raskin. 451-465 [doi]
• GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal FormulaeYih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Kang-Nien Wu, Wen-Chin Chan. 466-471 [doi]
• Faster Algorithms for Finitary GamesFlorian Horn. 472-484 [doi]
• Planned and Traversable Play-Out: A Flexible Method for Executing Scenario-Based Programs:::, :::David Harel, Itai Segall. 485-499 [doi]
• motor: The modestTool EnvironmentHenrik C. Bohnenkamp, Holger Hermanns, Joost-Pieter Katoen. 500-504 [doi]
• Syntactic Optimizations for PSL VerificationAlessandro Cimatti, Marco Roveri, Stefano Tonetta. 505-518 [doi]
• The Heterogeneous Tool Set, HetsTill Mossakowski, Christian Maeder, Klaus Lüttich. 519-522 [doi]
• Searching for Shapes in Cryptographic ProtocolsShaddin F. Doghmi, Joshua D. Guttman, F. Javier Thayer. 523-537 [doi]
• Automatic Analysis of the Security of XOR-Based Key Management SchemesVéronique Cortier, Gavin Keighren, Graham Steel. 538-552 [doi]
• State of the Union: Type Inference Via Craig InterpolationRanjit Jhala, Rupak Majumdar, Ru-Gang Xu. 553-567 [doi]
• Hoare Logic for Realistically Modelled Machine CodeMagnus O. Myreen, Michael J. C. Gordon. 568-582 [doi]
• VCEGAR: Verilog CounterExample Guided Abstraction RefinementHimanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke. 583-586 [doi]
• Alloy Analyzer+PVS in the Analysis and Verification of Alloy SpecificationsMarcelo F. Frias, Carlos López Pombo, Mariano M. Moscato. 587-601 [doi]
• Combined Satisfiability Modulo Parametric TheoriesSava Krstic, Amit Goel, Jim Grundy, Cesare Tinelli. 602-617 [doi]
• A Gröbner Basis Approach to CNF-Formulae PreprocessingChristopher Condrat, Priyank Kalla. 618-631 [doi]
• Kodkod: A Relational Model FinderEmina Torlak, Daniel Jackson. 632-647 [doi]
• Bounded Reachability Checking of Asynchronous Systems Using Decision DiagramsAndy Jinqing Yu, Gianfranco Ciardo, Gerald Lüttgen. 648-663 [doi]
• Model Checking on Trees with Path EquivalencesRajeev Alur, Pavol Cerný, Swarat Chaudhuri. 664-678 [doi]
• Uppaal/DMC- Abstraction-Based Heuristics for Directed Model CheckingSebastian Kupferschmid, Klaus Dräger, Jörg Hoffmann, Bernd Finkbeiner, Henning Dierks, Andreas Podelski, Gerd Behrmann. 679-682 [doi]
• Distributed Analysis with ::::mu:::: CRL: A Compendium of Case StudiesStefan Blom, Jens R. Calame, Bert Lisser, Simona Orzan, Jun Pang, Jaco van de Pol, Muhammad Torabi Dashti, Anton Wijs. 683-689 [doi]
• A Generic Framework for Reasoning About Dynamic Networks of Infinite-State ProcessesAhmed Bouajjani, Yan Jurski, Mihaela Sighireanu. 690-705 [doi]
• Unfolding Concurrent Well-Structured Transition SystemsFrédéric Herbreteau, Grégoire Sutre, The Quang Tran. 706-720 [doi]
• Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)Parosh Aziz Abdulla, Giorgio Delzanno, Noomene Ben Henda, Ahmed Rezine. 721-736 [doi]