Abstract is missing.
- Toward Practical Application of Formal Methods in Software Lifecycle ProcessesMario Tokoro. 1 [doi]
- Formal Methods in the Aerospace Industry: Follow the MoneyDarren D. Cofer. 2-3 [doi]
- Applying Term Rewriting to Speech Recognition of NumbersRobert E. Shostak. 4 [doi]
- Variable Permissions for Concurrency VerificationDuy-Khanh Le, Wei-Ngan Chin, Yong Meng Teo. 5-21 [doi]
- A Concurrent Temporal Programming Model with Atomic BlocksXiaoxiao Yang, Yu Zhang, Ming Fu, Xinyu Feng. 22-37 [doi]
- A Composable Mixed Mode Concurrency Control Semantics for Transactional ProgramsGranville Barnett, Shengchao Qin. 38-53 [doi]
- Towards a Formal Verification Methodology for Collective Robotic SystemsEdmond Gjondrekaj, Michele Loreti, Rosario Pugliese, Francesco Tiezzi, Carlo Pinciroli, Manuele Brambilla, Mauro Birattari, Marco Dorigo. 54-70 [doi]
- Modeling Resource-Aware Virtualized Applications for the Cloud in Real-Time ABSEinar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa. 71-86 [doi]
- Specification and Model Checking of the Chandy and Lamport Distributed Snapshot Algorithm in Rewriting LogicKazuhiro Ogata, Thi Thanh Huyen Phan. 87-102 [doi]
- Quantitative Program Dependence GraphsChunyan Mu. 103-118 [doi]
- Quantitative Analysis of Information Flow Using Theorem ProvingTarek Mhamdi, Osman Hasan, Sofiène Tahar. 119-134 [doi]
- Modeling and Verification of Probabilistic Actor Systems Using pRebecaMahsa Varshosaz, Ramtin Khosravi. 135-150 [doi]
- Modular Verification of OO Programs with InterfacesZongyan Qiu, Ali Hong, Yijing Liu. 151-166 [doi]
- Separation Predicates: A Taste of Separation Logic in First-Order LogicFrançois Bobot, Jean-Christophe Filliâtre. 167-181 [doi]
- The Confinement Problem in the Presence of FaultsWilliam L. Harrison, Adam M. Procter, Gerard Allwein. 182-197 [doi]
- Verification of ATL Transformations Using Transformation Models and Model FindersFabian Büttner, Marina Egea, Jordi Cabot, Martin Gogolla. 198-213 [doi]
- Automatic Generation of Provably Correct Embedded SystemsShang-Wei Lin, Yang Liu, Pao-Ann Hsiung, Jun Sun 0001, Jin Song Dong. 214-229 [doi]
- Complementary Methodologies for Developing Hybrid Systems with Event-BWen Su, Jean-Raymond Abrial, Huibiao Zhu. 230-248 [doi]
- A Temporal Logic with Mean-Payoff ConstraintsTakashi Tomita, Shin Hiura, Shigeki Hagihara, Naoki Yonezaki. 249-265 [doi]
- Time Constraints with Temporal Logic ProgrammingMeng Han, Zhenhua Duan, Xiaobing Wang. 266-282 [doi]
- Stepwise Satisfiability Checking Procedure for Reactive System Specifications by Tableau Method and Proof SystemYoshinori Neya, Noriaki Yoshiura. 283-298 [doi]
- Equational Abstraction Refinement for Certified Tree Regular Model CheckingYohan Boichut, Benoît Boyer, Thomas Genet, Axel Legay. 299-315 [doi]
- SMT-Based False Positive Elimination in Static Program AnalysisMaximilian Junker, Ralf Huuck, Ansgar Fehnker, Alexander Knapp. 316-331 [doi]
- Predicate Analysis with Block-Abstraction MemoizationDaniel Wonisch, Heike Wehrheim. 332-347 [doi]
- Heuristic-Guided Abstraction Refinement for Concurrent SystemsNils Timm, Heike Wehrheim, Mike Czech. 348-363 [doi]
- More Anti-chain Based Refinement CheckingTing Wang, Songzheng Song, Jun Sun 0001, Yang Liu, Jin Song Dong, Xinyu Wang, Shanping Li. 364-380 [doi]
- An Analytical and Experimental Comparison of CSP Extensions and ToolsLing Shi, Yang Liu, Jun Sun 0001, Jin Song Dong, Gustavo Carvalho. 381-397 [doi]
- Symbolic Model-Checking of Stateful Timed CSP Using BDD and DigitizationTruong Khanh Nguyen, Jun Sun 0001, Yang Liu, Jin Song Dong. 398-413 [doi]
- Annotations for Alloy: Automated Incremental Analysis Using Domain Specific SolversSvetoslav R. Ganov, Sarfraz Khurshid, Dewayne E. Perry. 414-429 [doi]
- State Space c-Reductions of Concurrent Systems in Rewriting LogicAlberto Lluch-Lafuente, José Meseguer, Andrea Vandin. 430-446 [doi]
- A Practical Loop Invariant Generation Approach Based on Random Testing, Constraint Solving and VerificationMengjun Li. 447-461 [doi]
- ConSMutate: SQL Mutants for Guiding Concolic Testing of Database ApplicationsTanmoy Sarkar, Samik Basu, Johnny S. Wong. 462-477 [doi]
- Demonic Testing of Concurrent ProgramsScott West, Sebastian Nanz, Bertrand Meyer. 478-493 [doi]
- Towards Certified Runtime VerificationJan Olaf Blech, Yliès Falcone, Klaus Becker. 494-509 [doi]