default search action
12th ICFEM 2010: Shanghai, China
- Jin Song Dong, Huibiao Zhu:
Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings. Lecture Notes in Computer Science 6447, Springer 2010, ISBN 978-3-642-16900-7
Invited Talks
- Kokichi Futatsugi:
Fostering Proof Scores in CafeOBJ. 1-20 - Matthew B. Dwyer:
Exploiting Partial Success in Applying Automated Formal Methods. 21 - Wang Yi:
Multicore Embedded Systems: The Timing Problem and Possible Solutions. 22-23
Theorem Proving and Decision Procedures
- Johannes Eriksson, Ralph-Johan Back:
Applying PVS Background Theories and Proof Strategies in Invariant Based Programming. 24-39 - Augusto Ribeiro, Peter Gorm Larsen:
Proof Obligation Generation and Discharging for Recursive Definitions in VDM. 40-55 - Iman Poernomo, Jeffrey Terrell:
Correct-by-Construction Model Transformations from Partially Ordered Specifications in Coq. 56-73 - Alejandro Sánchez, César Sánchez:
Decision Procedures for the Temporal Verification of Concurrent Lists. 74-89 - Zhenhua Duan, Cong Tian:
An Improved Decision Procedure for Propositional Projection Temporal Logic. 90-105
Web Services and Workflow
- Natallia Kokash, Behnaz Changizi, Farhad Arbab:
A Semantic Model for Service Composition with Coordination Time Delays. 106-121 - Fazle Rabbi, Hao Wang, Wendy MacCaull:
Compensable WorkFlow Nets. 122-137 - Lei Zhou, Jing Ping, Hao Xiao, Zheng Wang, Geguang Pu, Zuohua Ding:
Automatically Testing Web Services Choreography with Assertions. 138-154 - Zuohua Ding, Hui Shen, Jing Liu:
Applying Ordinary Differential Equations to the Performance Analysis of Service Composition. 155-170
Verification I
- Shengchao Qin, Chenguang Luo, Guanhua He, Florin Craciun, Wei-Ngan Chin:
Verifying Heap-Manipulating Programs with Unknown Procedure Calls. 171-187 - Xin Li, H. James Hoover, Piotr Rudnicki:
API Conformance Verification for Java Programs. 188-203 - Alessio Lomuscio, Ben Strulo, Nigel G. Walker, Peng Wu:
Assume-Guarantee Reasoning with Local Specifications. 204-219 - Eugen-Ioan Goriac, Dorel Lucanu, Grigore Rosu:
Automating Coinduction with Case Analysis. 220-236
Applications of Formal Methods
- Hai H. Wang, Danica Damljanovic, Jing Sun:
Enhanced Semantic Access to Formal Software Models. 237-252 - Denis Hatebur, Maritta Heisel:
Making Pattern- and Model-Based Software Development More Rigorous. 253-269 - Andi Bejleri:
Practical Parameterised Session Types. 270-286 - Ken Madlener, Sjaak Smetsers, Marko C. J. D. van Eekelen:
A Formal Verification Study on the Rotterdam Storm Surge Barrier. 287-302
Verification II
- José Meseguer, Peter Csaba Ölveczky:
Formalization and Correctness of the PALS Architectural Pattern for Distributed Real-Time Systems. 303-320 - Antti Siirtola:
Automated Multiparameterised Verification by Cut-Offs. 321-337 - Youssef Hanna, David Samuelson, Samik Basu, Hridesh Rajan:
Automating Cut-off for Multi-parameterized Systems. 338-354 - Miroslav N. Velev, Ping Gao:
Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors. 355-370 - Islam Abdelhalim, James Sharp, Steve A. Schneider, Helen Treharne:
Formal Verification of Tokeneer Behaviours Modelled in fUML Using CSP. 371-387
Probability and Concurrency
- Jun Sun, Songzheng Song, Yang Liu:
Model Checking Hierarchical Probabilistic Systems. 388-403 - Zijiang Yang, Karem A. Sakallah:
Trace-Driven Verification of Multithreaded Programs. 404-419 - Jonathan Billington, Guy Edward Gallasch:
Closed Form Approximations for Steady State Probabilities of a Controlled Fork-Join Network. 420-435 - Imene Ben Hafaiedh, Susanne Graf, Sophie Quinton:
Reasoning about Safety and Progress Using Contracts. 436-451
Program Analysis
- Isabella Mastroeni, Durica Nikolic:
Abstract Program Slicing: From Theory towards an Implementation. 452-467 - Shengchao Qin, Guanhua He, Chenguang Luo, Wei-Ngan Chin:
Loop Invariant Synthesis in a Combined Domain. 468-484 - Andreas Vogelsang, Ansgar Fehnker, Ralf Huuck, Wolfgang Reif:
Software Metrics in Static Program Analysis. 485-500 - Kazuhiro Ogata, Kokichi Futatsugi:
A Combination of Forward and Backward Reachability Analysis Methods. 501-517
Model Checking
- Jun Sun, Yang Liu, Bin Cheng:
Model Checking a Model Checker: A Code Contract Combined Approach. 518-533 - Nils Timm, Heike Wehrheim:
On Symmetries and Spotlights - Verifying Parameterised Systems. 534-548 - Jonathan Ezekiel, Alessio Lomuscio:
A Methodology for Automatic Diagnosability Analysis. 549-564 - Rüdiger Ehlers, Michael Gerke, Hans-Jörg Peter:
Making the Right Cut in Model Checking Data-Intensive Timed Systems. 565-580 - Marc Frappier, Benoît Fraikin, Romain Chossart, Raphaël Chane-Yack-Fa, Mohammed Ouenzar:
Comparison of Model Checking Tools for Information Systems. 581-596
Object Orientation and Model Driven Engineering
- Scott West, Sebastian Nanz, Bertrand Meyer:
A Modular Scheme for Deadlock Prevention in an Object-Oriented Programming Model. 597-612 - Prabhu Shankar Kaliappan, Hartmut König, Sebastian Schmerl:
Model-Driven Protocol Design Based on Component Oriented Modeling. 613-629 - Hong Zhu, Ian Bayley:
Laws of Pattern Composition. 630-645 - Einar Broch Johnsen, Olaf Owe, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa:
Dynamic Resource Reallocation between Deployment Components. 646-661
Specification and Verification
- Xi Wang, Shaoying Liu, Huaikou Miao:
A Pattern System to Support Refining Informal Ideas into Formal Expressions. 662-677 - Min Zhang, Kazuhiro Ogata, Masaki Nakamura:
Specification Translation of State Machines from Equational Theories into Rewrite Theories. 678-693 - Cong Tian, Zhenhua Duan:
Alternating Interval Based Temporal Logics. 694-709
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.