| Description |
1 online resource (xiv, 512 pages) : illustrations |
| Series |
Lecture notes in computer science ; 7635 |
|
LNCS sublibrary. SL 2, Programming and software engineering |
|
Lecture notes in computer science ; 7635
|
|
LNCS sublibrary. SL 2, Programming and software engineering
|
| Contents |
Invited Speech: Toward Practical Application of Formal Methods in Software Lifecycle Processes / Mario Tokoro -- Formal Methods in the Aerospace Industry: Follow the Money / Darren Cofer -- Applying Term Rewriting to Speech Recognition of Numbers / Robert E. Shostak -- Concurrency: Variable Permissions for Concurrency Verification / Duy-Khanh Le, Wei-Ngan Chin, Yong-Meng Teo -- A Concurrent Temporal Programming Model with Atomic Blocks / Xiaoxiao Yang, Yu Zhang, Ming Fu, Xinyu Feng -- A Composable Mixed Mode Concurrency Control Semantics for Transactional Programs / Granville Barnett, Shengchao Qin -- Applications of Formal Methods to New Areas: Towards a Formal Verification Methodology for Collective Robotic Systems / Edmond Gjondrekaj, Michele Loreti, Rosario Pugliese, Francesco Tiezzi, Carlo Pinciroli -- Modeling Resource-Aware Virtualized Applications for the Cloud in Real-Time ABS / Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa |
|
Specification and Model Checking of the Chandy and Lamport Distributed Snapshot Algorithm in Rewriting Logic / Kazuhiro Ogata, Phan Thi Thanh Huyen -- Quantity and Probability: Quantitative Program Dependence Graphs / Chunyan Mu -- Quantitative Analysis of Information Flow Using Theorem Proving / Tarek Mhamdi, Osman Hasan, Sofiène Tahar -- Modeling and Verification of Probabilistic Actor Systems Using pRebeca / Mahsa Varshosaz, Ramtin Khosravi -- Formal Verification: Modular Verification of OO Programs with Interfaces / Qiu Zongyan, Hong Ali, Liu Yijing -- Separation Predicates: A Taste of Separation Logic in First-Order Logic / François Bobot, Jean-Christophe Filliâtre -- The Confinement Problem in the Presence of Faults / William L. Harrison, Adam Procter, Gerard Allwein -- Modeling and Development Methodology: Verification of ATL Transformations Using Transformation Models and Model Finders / Fabian Büttner, Marina Egea, Jordi Cabot, Martin Gogolla |
|
Automatic Generation of Provably Correct Embedded Systems / Shang-Wei Lin, Yang Liu, Pao-Ann Hsiung, Jun Sun, Jin Song Dong -- Complementary Methodologies for Developing Hybrid Systems with Event-B / Wen Su, Jean-Raymond Abrial, Huibiao Zhu -- Temporal Logics: A Temporal Logic with Mean-Payoff Constraints / Takashi Tomita, Shin Hiura, Shigeki Hagihara, Naoki Yonezaki -- Time Constraints with Temporal Logic Programming / Meng Han, Zhenhua Duan, Xiaobing Wang -- Stepwise Satisfiability Checking Procedure for Reactive System Specifications by Tableau Method and Proof System / Yoshinori Neya, Noriaki Yoshiura -- Abstraction and Refinement: Equational Abstraction Refinement for Certified Tree Regular Model Checking / Yohan Boichut, Benoit Boyer, Thomas Genet, Axel Legay -- SMT-Based False Positive Elimination in Static Program Analysis / Maximilian Junker, Ralf Huuck, Ansgar Fehnker, Alexander Knapp -- Predicate Analysis with Block-Abstraction Memoization / Daniel Wonisch, Heike Wehrheim -- Heuristic-Guided Abstraction Refinement for Concurrent Systems / Nils Timm, Heike Wehrheim, Mike Czech |
|
More Anti-chain Based Refinement Checking / Ting Wang, Songzheng Song, Jun Sun, Yang Liu, Jin Song Dong, Xinyu Wang, Shanping Li -- Tools: An Analytical and Experimental Comparison of CSP Extensions and Tools / Ling Shi, Yang Liu, Jun Sun, Jin Song Dong, Gustavo Carvalho -- Symbolic Model-Checking of Stateful Timed CSP Using BDD and Digitization / Truong Khanh Nguyen, Jun Sun, Yang Liu, Jin Song Dong -- Annotations for Alloy: Automated Incremental Analysis Using Domain Specific Solvers / Svetoslav Ganov, Sarfraz Khurshid, Dewayne E. Perry -- State Space c-Reductions of Concurrent Systems in Rewriting Logic / Alberto Lluch Lafuente, José Meseguer, Andrea Vandin -- Testing and Runtime Verification: A Practical Loop Invariant Generation Approach Based on Random Testing, Constraint Solving and Verification / Mengjun Li -- ConSMutate: SQL Mutants for Guiding Concolic Testing of Database Applications / Tanmoy Sarkar, Samik Basu, Johnny S. Wong -- Demonic Testing of Concurrent Programs / Scott West, Sebastian Nanz, Bertrand Meyer -- Towards Certified Runtime Verification / Jan Olaf Blech, Ylies Falcone, Klaus Becker |
| Summary |
This book constitutes the refereed proceedings of the 14th International Conference on Formal Engineering Methods, ICFEM 2012, held in Kyoto, Japan, November 2012. The 31 revised full papers together with 3 invited talks presented were carefully reviewed and selected from 85 submissions. The papers address all current issues in formal methods and their applications in software engineering. They are organized in topical sections on concurrency, applications of formal methods to new areas, quantity and probability, formal verification, modeling and development methodology, temporal logics, abstraction and refinement, tools, as well as testing and runtime verification |
| Bibliography |
Includes bibliographical references and author index |
| Notes |
Online resource; title from digital title page (viewed on November 9, 2012) |
| In |
Springer eBooks |
| Subject |
Formal methods (Computer science) -- Congresses
|
|
Software engineering -- Congresses
|
|
Computer software -- Verification -- Congresses
|
|
COMPUTERS -- Programming -- Open Source.
|
|
COMPUTERS -- Software Development & Engineering -- General.
|
|
COMPUTERS -- Software Development & Engineering -- Tools.
|
|
Informatique.
|
|
Computer software -- Verification
|
|
Formal methods (Computer science)
|
|
Software engineering
|
| Genre/Form |
Conference papers and proceedings
|
|
Software.
|
| Form |
Electronic book
|
| Author |
Aoki, Toshiaki
|
|
Taguchi, Kenji, 1956-
|
| ISBN |
9783642342813 |
|
3642342817 |
|
