Abstract is missing.
- Statistical Model Checking for Cyber-Physical SystemsEdmund M. Clarke, Paolo Zuliani. 1-12 [doi]
- Max and Sum Semantics for Alternating Weighted AutomataShaull Almagor, Orna Kupferman. 13-27 [doi]
- Making Software Verification Tools Really WorkJade Alglave, Alastair F. Donaldson, Daniel Kroening, Michael Tautschnig. 28-42 [doi]
- Synthesizing, Verifying, and Debugging SoC with FSM-Based Specification of On-Chip Communication ProtocolsMasahiro Fujita. 43-50 [doi]
- Automated Analysis of Industrial Embedded SoftwareMoonzoo Kim, Yunho Kim. 51-59 [doi]
- Nondeterministic Update of CTL Models by Preserving Satisfaction through ProtectionsMiguel A. Carrillo, David A. Rosenblueth. 60-74 [doi]
- Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic ProtocolsMorten Dahl, Naoki Kobayashi 0001, Yunde Sun, Hans Hüttel. 75-89 [doi]
- Formalization of Finite-State Discrete-Time Markov Chains in HOLLiya Liu, Osman Hasan, Sofiène Tahar. 90-104 [doi]
- An Alternative Definition for Timed Automata CompositionJean-Paul Bodeveix, Abdeldjalil Boudjadar, Mamoun Filali. 105-119 [doi]
- Model Checking EGF on Basic Parallel ProcessesHongfei Fu. 120-134 [doi]
- Measuring Permissiveness in Parity Games: Mean-Payoff Parity Games RevisitedPatricia Bouyer, Nicolas Markey, Jörg Olschewski, Michael Ummels. 135-149 [doi]
- Algorithms for Synthesizing Priorities in Component-Based SystemsChih-Hong Cheng, Saddek Bensalem, Yu-Fang Chen, Rongjie Yan, Barbara Jobstmann, Harald Ruess, Christian Buckl, Alois Knoll. 150-167 [doi]
- Trust Metrics for the SPKI/SDSI Authorisation FrameworkDominik Wojtczak. 168-182 [doi]
- Antichain-Based QBF SolvingThomas Brihaye, Véronique Bruyère, Laurent Doyen 0001, Marc Ducobu, Jean-François Raskin. 183-197 [doi]
- A Hierarchical Approach for the Synthesis of Stabilizing Controllers for Hybrid SystemsJanusz Malinowski, Peter Niebert, Pierre-Alain Reynier. 198-212 [doi]
- Formal Analysis of Online AlgorithmsBenjamin Aminof, Orna Kupferman, Robby Lampert. 213-227 [doi]
- Modal Transition Systems: Composition and LTL Model CheckingNikola Benes, Ivana Cerná, Jan Kretínský. 228-242 [doi]
- Efficient Inclusion Checking on Explicit and Semi-symbolic Tree AutomataLukás Holík, Ondrej Lengál, Jirí Simácek, Tomás Vojnar. 243-258 [doi]
- Assembling SessionsPhilippe Darondeau, Loïc Hélouët, Madhavan Mukund. 259-274 [doi]
- Parametric Modal Transition SystemsNikola Benes, Jan Kretínský, Kim G. Larsen, Mikael H. Møller, Jirí Srba. 275-289 [doi]
- Policy Iteration within Logico-Numerical Abstract DomainsPascal Sotin, Bertrand Jeannet, Franck Védrine, Eric Goubault. 290-305 [doi]
- Small Strategies for Safety GamesDaniel Neider. 306-320 [doi]
- Multi-core Nested Depth-First SearchAlfons Laarman, Rom Langerak, Jaco van de Pol, Michael Weber 0002, Anton Wijs. 321-335 [doi]
- Self-Loop Aggregation Product - A New Hybrid Approach to On-the-Fly LTL Model CheckingAlexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, Yann Thierry-Mieg. 336-350 [doi]
- A Lightweight Approach for Loop SummarizationMohamed Nassim Seghir. 351-365 [doi]
- A Succinct Canonical Register Automaton ModelSofia Cassel, Falk Howar, Bengt Jonsson, Maik Merten, Bernhard Steffen. 366-380 [doi]
- Parallel Nested Depth-First Searches for LTL Model CheckingSami Evangelista, Laure Petrucci, Samir Youcef. 381-396 [doi]
- Evaluating LTL Satisfiability SolversViktor Schuppan, Luthfi Darmawan. 397-413 [doi]
- McAiT - A Timing Analyzer for Multicore Real-Time SoftwareMingsong Lv, Nan Guan, Qingxu Deng, Ge Yu, Wang Yi 0001. 414-417 [doi]
- MIO Workbench: A Tool for Compositional Design with Modal Input/Output InterfacesSebastian S. Bauer, Philip Mayer, Axel Legay. 418-421 [doi]
- The Buck Stops Here: Order, Chance, and Coordination in Distributed ControlGal Katz, Doron Peled, Sven Schewe. 422-431 [doi]
- Symbolic Verification and Test Generation for a Network of Communicating FSMsXiaoqing Jin, Gianfranco Ciardo, Tae-Hyong Kim, Yang Zhao. 432-442 [doi]
- Hierarchical Counterexamples for Discrete-Time Markov ChainsNils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. 443-452 [doi]
- Efficient Loop Navigation for Symbolic ExecutionJan Obdrzálek, Marek Trtík. 453-462 [doi]
- An Efficient Algorithm for Learning Event-Recording AutomataShang-Wei Lin, Étienne André, Jin Song Dong, Jun Sun 0001, Yang Liu 0003. 463-472 [doi]
- Discretizing Affine Hybrid Automata with UncertaintyThao Dang, Thomas Martin Gawlitza. 473-481 [doi]
- What's Decidable about Weighted Automata?Shaull Almagor, Udi Boker, Orna Kupferman. 482-491 [doi]
- Widening with Thresholds for Programs with Complex Control GraphsLies Lakhdar-Chaouch, Bertrand Jeannet, Alain Girault. 492-502 [doi]
- Linear Hybrid System Falsification through Local SearchHoussam Abbas, Georgios E. Fainekos. 503-510 [doi]
- Learning-Based Compositional Verification for Synchronous Probabilistic SystemsLu Feng, Tingting Han, Marta Z. Kwiatkowska, David Parker. 511-521 [doi]
- An Algorithmic Framework for Synthesis of Concurrent ProgramsE. Allen Emerson, Roopsha Samanta. 522-530 [doi]