Abstract is missing.
- Transactional Memory: Glimmer of a TheoryRachid Guerraoui, Michal Kapalka. 1-15 [doi]
- Mixed-Signal System Verification: A High-Speed Link ExampleJaeha Kim. 16 [doi]
- Modelling Epigenetic Information Maintenance: A Kappa TutorialJean Krivine, Vincent Danos, Arndt Benecke. 17-32 [doi]
- Component-Based Construction of Real-Time Systems in BIPJoseph Sifakis. 33-34 [doi]
- Models and Proofs of Protocol Security: A Progress ReportMartín Abadi, Bruno Blanchet, Hubert Comon-Lundh. 35-49 [doi]
- Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after?Luca Benini. 50 [doi]
- SPEED: Symbolic Complexity Bound AnalysisSumit Gulwani. 51-62 [doi]
- Regression Verification: Proving the Equivalence of Similar ProgramsOfer Strichman. 63 [doi]
- Symbolic Counter Abstraction for Concurrent SoftwareGérard Basler, Michele Mazzucchi, Thomas Wahl, Daniel Kroening. 64-78 [doi]
- Priority Scheduling of Distributed Systems Based on Model CheckingAnanda Basu, Saddek Bensalem, Doron Peled, Joseph Sifakis. 79-93 [doi]
- Explaining Counterexamples Using CausalityIlan Beer, Shoham Ben-David, Hana Chockler, Avigail Orni, Richard J. Trefler. 94-108 [doi]
- Size-Change Termination, Monotonicity Constraints and Ranking FunctionsAmir M. Ben-Amram. 109-123 [doi]
- Linear Functional Fixed-pointsNikolaj Bjørner, Joe Hendrix. 124-139 [doi]
- Better Quality in Synthesis through Quantitative ObjectivesRoderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann. 140-156 [doi]
- Automatic Verification of Integer Array ProgramsMarius Bozga, Peter Habermehl, Radu Iosif, Filip Konecný, Tomás Vojnar. 157-172 [doi]
- Automated Analysis of Java Methods for ConfidentialityPavol Cerný, Rajeev Alur. 173-187 [doi]
- Requirements Validation for Hybrid SystemsAlessandro Cimatti, Marco Roveri, Stefano Tonetta. 188-203 [doi]
- Towards Performance Prediction of Compositional Models in Industrial GALS DesignsNicolas Coste, Holger Hermanns, Etienne Lantreibecq, Wendelin Serwe. 204-218 [doi]
- Image Computation for Polynomial Dynamical Systems Using the Bernstein ExpansionThao Dang, David Salinas. 219-232 [doi]
- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over IntegersIsil Dillig, Thomas Dillig, Alex Aiken. 233-247 [doi]
- Meta-analysis for Atomicity Violations under Nested LockingAzadeh Farzan, P. Madhusudan, Francesco Sorrentino. 248-262 [doi]
- An Antichain Algorithm for LTL RealizabilityEmmanuel Filiot, Naiyong Jin, Jean-François Raskin. 263-277 [doi]
- On Extending Bounded Proofs to Inductive ProofsOded Fuhrmann, Shlomo Hoory. 278-290 [doi]
- Games through Nested FixpointsThomas Gawlitza, Helmut Seidl. 291-305 [doi]
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo TheoriesYeting Ge, Leonardo Mendonça de Moura. 306-320 [doi]
- Software Transactional Memory on Relaxed Memory ModelsRachid Guerraoui, Thomas A. Henzinger, Vasu Singh. 321-336 [doi]
- Sliding Window Abstraction for Infinite Markov ChainsThomas A. Henzinger, Maria Mateescu, Verena Wolf. 337-352 [doi]
- Centaur Technology Media Unit VerificationWarren A. Hunt Jr., Sol Swords. 353-367 [doi]
- Incremental Instance Generation in Local ReasoningSwen Jacobs. 368-382 [doi]
- Quantifier Elimination via Functional CompositionJie-Hong R. Jiang. 383-397 [doi]
- Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction TechniqueVineet Kahlon, Chao Wang, Aarti Gupta. 398-413 [doi]
- Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine ValidationRoope Kaivola, Rajnish Ghughal, Naren Narasimhan, Amber Telfer, Jesse Whittemore, Sudhindra Pandav, Anna Slobodová, Christopher Taylor, Vladimir Frolov, Erik Reeber, Armaghan Naik. 414-429 [doi]
- Generating and Analyzing Symbolic Traces of Simulink/Stateflow ModelsAditya Kanade, Rajeev Alur, Franjo Ivančić, S. Ramesh, Sriram Sankaranarayanan, K. C. Shashidhar. 430-445 [doi]
- A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer ConstraintsNathan Kitchen, Andreas Kuehlmann. 446-461 [doi]
- Generalizing DPLL to Richer LogicsKenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv. 462-476 [doi]
- Reducing Context-Bounded Concurrent Reachability to Sequential ReachabilitySalvatore La Torre, P. Madhusudan, Gennaro Parlato. 477-492 [doi]
- Intra-module InferenceShuvendu K. Lahiri, Shaz Qadeer, Juan P. Galeotti, Jan W. Voung, Thomas Wies. 493-508 [doi]
- Static and Precise Detection of Concurrency Errors in Systems Code Using SMT SolversShuvendu K. Lahiri, Shaz Qadeer, Zvonimir Rakamaric. 509-524 [doi]
- Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular ConstraintsPeter Lammich, Markus Müller-Olm, Alexander Wenner. 525-539 [doi]
- Reachability Analysis of Hybrid Systems Using Support FunctionsColas Le Guernic, Antoine Girard. 540-554 [doi]
- Reducing Test Inputs Using Information PartitionsRupak Majumdar, Ru-Gang Xu. 555-569 [doi]
- On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision ProcedureDavid Monniaux. 570-583 [doi]
- Cardinality Abstraction for Declarative Networking ApplicationsJuan Antonio Navarro Pérez, Andrey Rybalchenko, Atul Singh. 584-598 [doi]
- Equivalence Checking of Static Affine Programs Using Widening to Handle RecurrencesSven Verdoolaege, Gerda Janssens, Maurice Bruynooghe. 599-613 [doi]
- D-Finder: A Tool for Compositional Deadlock Detection and VerificationSaddek Bensalem, Marius Bozga, Thanh-Hung Nguyen, Joseph Sifakis. 614-619 [doi]
- HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous EnvironmentOlivier Bouissou, Eric Goubault, Sylvie Putot, Karim Tekkal, Franck Védrine. 620-626 [doi]
- The Zonotope Abstract Domain Taylor1+Khalil Ghorbal, Eric Goubault, Sylvie Putot. 627-633 [doi]
- InvGen: An Efficient Invariant GeneratorAshutosh Gupta, Andrey Rybalchenko. 634-640 [doi]
- INFAMY: An Infinite-State Markov Model CheckerErnst Moritz Hahn, Holger Hermanns, Björn Wachter, Lijun Zhang. 641-647 [doi]
- Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeepSylvain Hallé, Roger Villemaire. 648-653 [doi]
- Homer: A Higher-Order Observational Equivalence Model checkERDavid Hopkins, C.-H. Luke Ong. 654-660 [doi]
- Apron: A Library of Numerical Abstract Domains for Static AnalysisBertrand Jeannet, Antoine Miné. 661-667 [doi]
- Beaver: Engineering an Efficient SMT Solver for Bit-Vector ArithmeticSusmit Jha, Rhishikesh Limaye, Sanjit A. Seshia. 668-674 [doi]
- CalFuzzer: An Extensible Active Testing Framework for Concurrent ProgramsPallavi Joshi, Mayur Naik, Chang-Seo Park, Koushik Sen. 675-681 [doi]
- MCMAS: A Model Checker for the Verification of Multi-Agent SystemsAlessio Lomuscio, Hongyang Qu, Franco Raimondi. 682-688 [doi]
- TASS: Timing Analyzer of Scenario-Based SpecificationsMinxue Pan, Lei Bu, Xuandong Li. 689-695 [doi]
- Translation Validation: From Simulink to CMichael Ryabtsev, Ofer Strichman. 696-701 [doi]
- VS3: SMT Solvers for Program VerificationSaurabh Srivastava, Sumit Gulwani, Jeffrey S. Foster. 702-708 [doi]
- PAT: Towards Flexible Verification under FairnessJun Sun 0001, Yang Liu, Jin Song Dong, Jun Pang. 709-714 [doi]
- A Concurrent Portfolio Approach to SMT SolvingChristoph M. Wintersteiger, Youssef Hamadi, Leonardo Mendonça de Moura. 715-720 [doi]