Abstract is missing.
- Approximations for Stochastic Graph RewritingVincent Danos, Tobias Heindel, Ricardo Honorato-Zimmer, Sandro Stucki. 1-10 [doi]
- Computing Maximal BisimulationsAlexandre Boulgakov, Thomas Gibson-Robinson, A. W. Roscoe. 11-26 [doi]
- Improving the Model Checking of Strategies under Partial Observability and Fairness ConstraintsSimon Busard, Charles Pecheur, Hongyang Qu, Franco Raimondi. 27-42 [doi]
- A Formal Model for Natural-Language Timed Requirements of Reactive SystemsGustavo Carvalho, Ana Carvalho, Eduardo Rocha, Ana Cavalcanti, Augusto Sampaio. 43-58 [doi]
- A Hybrid Model of Connectors in Cyber-Physical SystemsXiaohong Chen, Jun Sun, Meng Sun. 59-74 [doi]
- A Language-Independent Proof System for Mutual Program EquivalenceStefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu. 75-90 [doi]
- PHASE: A Stochastic Formalism for Phase-Type DistributionsGabriel Ciobanu, Armand Stefan Rotaru. 91-106 [doi]
- CASSANDRA: An Online Failure Prediction Strategy for Dynamically Evolving SystemsFrancesco De Angelis, Maria Rita Di Berardini, Henry Muccini, Andrea Polini. 107-122 [doi]
- Modal Characterisations of Probabilistic and Fuzzy BisimulationsYuxin Deng, Hengyang Wu. 123-138 [doi]
- Pointer Program Derivation Using Coq: Graphs and Schorr-Waite AlgorithmJean-François Dufourd. 139-154 [doi]
- An LTL Model Checking Approach for Biological Parameter InferenceEmmanuelle Gallet, Matthieu Manceny, Pascale Le Gall, Paolo Ballarini. 155-170 [doi]
- SCC-Based Improved Reachability Analysis for Markov Decision ProcessesLin Gui, Jun Sun 0001, Songzheng Song, Yang Liu 0003, Jin Song Dong. 171-186 [doi]
- Comprehension of Spacecraft Telemetry Using Hierarchical Specifications of BehaviorKlaus Havelund, Rajeev Joshi. 187-202 [doi]
- Timed Automata Verification via IC3 with ZonesTobias Isenberg 0002, Heike Wehrheim. 203-218 [doi]
- GRL: A Specification Language for Globally Asynchronous Locally Synchronous SystemsFatma Jebali, Frédéric Lang, Radu Mateescu. 219-234 [doi]
- A Formal Framework to Prove the Correctness of Model Driven Engineering Composition OperatorsMounira Kezadri Hamiaz, Marc Pantel, Benoît Combemale, Xavier Thirioux. 235-250 [doi]
- A Formula-Based Approach for Automatic Fault Localization of Imperative ProgramsSi-Mohamed Lamraoui, Shin Nakajima. 251-266 [doi]
- A Resource-Based Logic for Termination and Non-termination ProofsTon Chanh Le, Cristian Gherghina, Aquinas Hobor, Wei-Ngan Chin. 267-283 [doi]
- Practical Analysis Framework for Software-Based Attestation SchemeLi Li, Hong Hu, Jun Sun, Yang Liu, Jin Song Dong. 284-299 [doi]
- TAuth: Verifying Timed Security ProtocolsLi Li, Jun Sun, Yang Liu, Jin Song Dong. 300-315 [doi]
- On the Formal Analysis of HMM Using Theorem ProvingLiya Liu, Vincent Aravantinos, Osman Hasan, Sofiène Tahar. 316-331 [doi]
- Formal Modeling and Analysis of Cassandra in MaudeSi Liu, Muntasir Raihan Rahman, Stephen Skeirik, Indranil Gupta, José Meseguer. 332-347 [doi]
- Bounded Model Checking High Level Petri Nets in PIPE+VerifierSu Liu, Reng Zeng, Zhuo Sun, Xudong He. 348-363 [doi]
- Fast Translation from LTL to Büchi Automata via Non-transition-based AutomataShohei Mochizuki, Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki. 364-379 [doi]
- Complete Model-Based Equivalence Class Testing for the ETCS Ceiling Speed MonitorCécile Braunstein, Anne Elisabeth Haxthausen, Wen-ling Huang, Felix Hübner, Jan Peleska, Uwe Schulze, Linh Vu Hong. 380-395 [doi]
- Contract-Based Verification of MATLAB and Simulink Matrix-Manipulating CodeJonatan Wiik, Pontus Boström. 396-412 [doi]
- GPU Accelerated Counterexample Generation in LTL Model CheckingZhimin Wu, Yang Liu, Yun Liang, Jun Sun 0001. 413-429 [doi]
- Formal Throughput and Response Time Analysis of MARTE ModelsGaogao Yan, Xueyang Zhu, Rongjie Yan, Guangyuan Li. 430-445 [doi]
- Extending MSVL with Function CallsNan Zhang, Zhenhua Duan, Cong Tian. 446-458 [doi]