Abstract is missing.
- Policies and Proofs for Code AuditingNathan Whitehead, Jordan Johnson, Martín Abadi. 1-14 [doi]
- Recent Trend in Industry and Expectation to DA ResearchAtsushi Hasegawa. 15-16 [doi]
- Toward Property-Driven Abstraction for Heap Manipulating ProgramsKenneth L. McMillan. 17-18 [doi]
- Branching vs. Linear Time: Semantical PerspectiveSumit Nain, Moshe Y. Vardi. 19-34 [doi]
- Mind the Shapes: Abstraction Refinement Via Topology InvariantsJörg Bauer, Tobe Toben, Bernd Westphal. 35-50 [doi]
- Complete SAT-Based Model Checking for Context-Free ProcessesGeng-Dian Huang, Bow-Yaw Wang. 51-65 [doi]
- Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT SolverDavid Walter, Scott Little, Chris J. Myers. 66-81 [doi]
- Model Checking Contracts - A Case StudyGordon J. Pace, Cristian Prisacariu, Gerardo Schneider. 82-97 [doi]
- On the Efficient Computation of the Minimal Coverability Set for Petri NetsGilles Geeraerts, Jean-François Raskin, Laurent Van Begin. 98-113 [doi]
- Analog/Mixed-Signal Circuit Verification Using Models Generated from Simulation TracesScott Little, David Walter, Kevin Jones, Chris J. Myers. 114-128 [doi]
- Automatic Merge-Point Detection for Sequential Equivalence Checking of System-Level and RTL DescriptionsBijan Alizadeh, Masahiro Fujita. 129-144 [doi]
- Proving Termination of Tree Manipulating ProgramsPeter Habermehl, Radu Iosif, Adam Rogalewicz, Tomás Vojnar. 145-161 [doi]
- Symbolic Fault Tree Analysis for Reactive SystemsMarco Bozzano, Alessandro Cimatti, Francesco Tapparo. 162-176 [doi]
- Computing Game Values for Crash GamesThomas Gawlitza, Helmut Seidl. 177-191 [doi]
- Timed Control with Observation Based and Stuttering Invariant StrategiesFranck Cassez, Alexandre David, Kim Guldstrand Larsen, Didier Lime, Jean-François Raskin. 192-206 [doi]
- Deciding Simulations on Probabilistic AutomataLijun Zhang, Holger Hermanns. 207-222 [doi]
- Mechanizing the Powerset Construction for Restricted Classes of ::::omega:::: -AutomataChristian Dax, Jochen Eisinger, Felix Klaedtke. 223-236 [doi]
- Verifying Heap-Manipulating Programs in an SMT FrameworkZvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti. 237-252 [doi]
- A Generic Constructive Solution for Concurrent Games with Expressive Constraints on StrategiesSophie Pinchinat. 253-267 [doi]
- Distributed Synthesis for Alternating-Time LogicsSven Schewe, Bernd Finkbeiner. 268-283 [doi]
- Timeout and Calendar Based Finite State Modeling and Verification of Real-Time SystemsIndranil Saha, Janardan Misra, Suman Roy. 284-299 [doi]
- Efficient Approximate Verification of Promela Models Via Symmetry MarkersDragan Bosnacki, Alastair F. Donaldson, Michael Leuschel, Thierry Massart. 300-315 [doi]
- Latticed Simulation Relations and GamesOrna Kupferman, Yoad Lustig. 316-330 [doi]
- Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model CheckingTingting Han, Joost-Pieter Katoen. 331-346 [doi]
- Assertion-Based Proof Checking of Chang-Roberts Leader Election in PVSJudi Romijn, Wieger Wesselink, Arjan J. Mooij. 347-361 [doi]
- Continuous Petri Nets: Expressive Power and Decidability IssuesLaura Recalde, Serge Haddad, Manuel Silva. 362-377 [doi]
- Quantifying the Discord: Order Discrepancies in Message Sequence ChartsEdith Elkind, Blaise Genest, Doron Peled, Paola Spoletini. 378-393 [doi]
- A Formal Methodology to Test Complex Heterogeneous SystemsIsmael Rodríguez, Manuel Núñez. 394-409 [doi]
- A New Approach to Bounded Model Checking for Branching Time LogicsRotem Oshman, Orna Grumberg. 410-424 [doi]
- Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State SpaceWerner Damm, Stefan Disch, Hardi Hungar, Swen Jacobs, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz. 425-440 [doi]
- A Compositional Semantics for Dynamic Fault Trees in Terms of Interactive Markov ChainsHichem Boudali, Pepijn Crouzen, Mariëlle Stoelinga. 441-456 [doi]
- 3-Valued Circuit SAT for STE with Automatic RefinementOrna Grumberg, Assaf Schuster, Avi Yadgar. 457-473 [doi]
- Bounded SynthesisSven Schewe, Bernd Finkbeiner. 474-488 [doi]
- Formal Modeling and Verification of High-Availability Protocol for Network Security AppliancesMoonzoo Kim. 489-500 [doi]
- A Brief Introduction to ::::THOTL::::Mercedes G. Merayo, Manuel Núñez, Ismael Rodríguez. 501-510 [doi]
- On-the-Fly Model Checking of Fair Non-repudiation ProtocolsGuoqiang Li, Mizuhito Ogawa. 511-522 [doi]
- Model Checking Bounded Prioritized Time Petri NetsBernard Berthomieu, Florent Peres, François Vernadat. 523-532 [doi]
- Using Patterns and Composite Propositions to Automate the Generation of LTL SpecificationsSalamah Salamah, Ann Q. Gates, Vladik Kreinovich, Steve Roach. 533-542 [doi]
- Pruning State Spaces with Extended Beam SearchMuhammad Torabi Dashti, Anton Wijs. 543-552 [doi]
- Using Counterexample Analysis to Minimize the Number of Predicates for Predicate AbstractionThanyapat Sakunkonchak, Satoshi Komatsu, Masahiro Fujita. 553-563 [doi]