


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

, Rosario Pugliese
, Francesco Tiezzi, Carlo Pinciroli, Manuele Brambilla, Mauro Birattari
, Marco Dorigo
:
Towards a Formal Verification Methodology for Collective Robotic Systems. 54-70 - Einar Broch Johnsen

, Rudolf Schlatte
, Silvia Lizeth Tapia Tarifa
:
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

, Sofiène Tahar:
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

, Jean-Christophe Filliâtre:
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

, Martin Gogolla:
Verification of ATL Transformations Using Transformation Models and Model Finders. 198-213 - Shang-Wei Lin

, Yang Liu
, Pao-Ann Hsiung
, Jun Sun
, Jin Song Dong:
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

, Shin Hiura, Shigeki Hagihara, Naoki Yonezaki:
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

, Alexander Knapp:
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

, Yang Liu
, Jin Song Dong, Xinyu Wang, Shanping Li:
More Anti-chain Based Refinement Checking. 364-380
Tools
- Ling Shi, Yang Liu

, Jun Sun
, Jin Song Dong, Gustavo Carvalho:
An Analytical and Experimental Comparison of CSP Extensions and Tools. 381-397 - Truong Khanh Nguyen, Jun Sun

, Yang Liu
, Jin Song Dong:
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

, José Meseguer, Andrea Vandin
:
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

, Yliès Falcone, Klaus Becker:
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.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














