default search action
14th ICFEM 2012: Kyoto, Japan
- Toshiaki Aoki, Kenji Taguchi:
Formal Methods and Software Engineering - 14th International Conference on Formal Engineering Methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012. Proceedings. Lecture Notes in Computer Science 7635, Springer 2012, ISBN 978-3-642-34280-6
Invited Speech
- Mario Tokoro:
Toward Practical Application of Formal Methods in Software Lifecycle Processes. 1 - Darren D. Cofer:
Formal Methods in the Aerospace Industry: Follow the Money. 2-3 - Robert E. Shostak:
Applying Term Rewriting to Speech Recognition of Numbers. 4
Concurrency
- Duy-Khanh Le, Wei-Ngan Chin, Yong Meng Teo
:
Variable Permissions for Concurrency Verification. 5-21 - Xiaoxiao Yang, Yu Zhang, Ming Fu, Xinyu Feng:
A Concurrent Temporal Programming Model with Atomic Blocks. 22-37 - Granville Barnett, Shengchao Qin
A Composable Mixed Mode Concurrency Control Semantics for Transactional Programs. 38-53
Applications of Formal Methods to New Areas
- Edmond Gjondrekaj, Michele Loreti
Towards a Formal Verification Methodology for Collective Robotic Systems. 54-70 - Einar Broch Johnsen
Modeling Resource-Aware Virtualized Applications for the Cloud in Real-Time ABS. 71-86 - Kazuhiro Ogata, Thi Thanh Huyen Phan:
Specification and Model Checking of the Chandy and Lamport Distributed Snapshot Algorithm in Rewriting Logic. 87-102
Quantity and Probability
- Chunyan Mu:
Quantitative Program Dependence Graphs. 103-118 - Tarek Mhamdi, Osman Hasan
Quantitative Analysis of Information Flow Using Theorem Proving. 119-134 - Mahsa Varshosaz, Ramtin Khosravi:
Modeling and Verification of Probabilistic Actor Systems Using pRebeca. 135-150
Formal Verification
- Zongyan Qiu, Ali Hong, Yijing Liu:
Modular Verification of OO Programs with Interfaces. 151-166 - François Bobot
Separation Predicates: A Taste of Separation Logic in First-Order Logic. 167-181 - William L. Harrison, Adam M. Procter, Gerard Allwein:
The Confinement Problem in the Presence of Faults. 182-197
Modeling and Development Methodology
- Fabian Büttner, Marina Egea, Jordi Cabot
Verification of ATL Transformations Using Transformation Models and Model Finders. 198-213 - Shang-Wei Lin
Automatic Generation of Provably Correct Embedded Systems. 214-229 - Wen Su, Jean-Raymond Abrial, Huibiao Zhu:
Complementary Methodologies for Developing Hybrid Systems with Event-B. 230-248
Temporal Logics
- Takashi Tomita
A Temporal Logic with Mean-Payoff Constraints. 249-265 - Meng Han, Zhenhua Duan, Xiaobing Wang:
Time Constraints with Temporal Logic Programming. 266-282 - Yoshinori Neya, Noriaki Yoshiura:
Stepwise Satisfiability Checking Procedure for Reactive System Specifications by Tableau Method and Proof System. 283-298
Abstraction and Refinement
- Yohan Boichut, Benoît Boyer, Thomas Genet, Axel Legay:
Equational Abstraction Refinement for Certified Tree Regular Model Checking. 299-315 - Maximilian Junker, Ralf Huuck, Ansgar Fehnker
SMT-Based False Positive Elimination in Static Program Analysis. 316-331 - Daniel Wonisch, Heike Wehrheim:
Predicate Analysis with Block-Abstraction Memoization. 332-347 - Nils Timm, Heike Wehrheim, Mike Czech:
Heuristic-Guided Abstraction Refinement for Concurrent Systems. 348-363 - Ting Wang, Songzheng Song, Jun Sun
More Anti-chain Based Refinement Checking. 364-380
Tools
- Ling Shi, Yang Liu
An Analytical and Experimental Comparison of CSP Extensions and Tools. 381-397 - Truong Khanh Nguyen, Jun Sun
Symbolic Model-Checking of Stateful Timed CSP Using BDD and Digitization. 398-413 - Svetoslav R. Ganov, Sarfraz Khurshid, Dewayne E. Perry:
Annotations for Alloy: Automated Incremental Analysis Using Domain Specific Solvers. 414-429 - Alberto Lluch-Lafuente
State Space c-Reductions of Concurrent Systems in Rewriting Logic. 430-446
Testing and Runtime Verification
- Mengjun Li:
A Practical Loop Invariant Generation Approach Based on Random Testing, Constraint Solving and Verification. 447-461 - Tanmoy Sarkar, Samik Basu, Johnny S. Wong:
ConSMutate: SQL Mutants for Guiding Concolic Testing of Database Applications. 462-477 - Scott West, Sebastian Nanz, Bertrand Meyer:
Demonic Testing of Concurrent Programs. 478-493 - Jan Olaf Blech
Towards Certified Runtime Verification. 494-509
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-10-02 20:31 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: