|
" Formal Methods and Software Engineering : "
Toshiaki Aoki ... (eds.).
| Document Type
|
:
|
BL
|
| Record Number
|
:
|
747663
|
| Doc. No
|
:
|
b567614
|
| Main Entry
|
:
|
Toshiaki Aoki ... (eds.).
|
| Title & Author
|
:
|
Formal Methods and Software Engineering : : 14th International Conference on Formal Engineering Methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012 ; proceedings\ Toshiaki Aoki ... (eds.).
|
| Publication Statement
|
:
|
Berlin : Springer, 2012
|
| Series Statement
|
:
|
Lecture Notes in Computer Science, 7635.
|
| ISBN
|
:
|
3642342809
|
|
|
:
|
: 3642342817
|
|
|
:
|
: 9783642342806
|
|
|
:
|
: 9783642342813
|
| Contents
|
:
|
Toward Practical Application of Formal Methods in Software Lifecycle Processes.- Formal Methods in the Aerospace Industry: Follow the Money.- Applying Term Rewriting to Speech Recognition of Numbers.- Variable Permissions for Concurrency Verification.- A Concurrent Temporal Programming Model with Atomic Blocks.- A Composable Mixed Mode Concurrency Control Semantics for Transactional Programs.- Towards a Formal Verification Methodology for Collective Robotic Systems.- Modeling Resource-Aware Virtualized Applications for the Cloud in Real-Time ABS.- Specification and Model Checking of the Chandy and Lamport Distributed Snapshot Algorithm in Rewriting Logic.- Quantitative Program Dependence Graphs.- Quantitative Analysis of Information Flow Using Theorem Proving.- Modeling and Verification of Probabilistic Actor Systems Using pRebeca.- Modular Verification of OO Programs with Interfaces.- Separation Predicates: A Taste of Separation Logic in First-OrderLogic.- The Confinement Problem in the Presence of Faults.- Verification of ATL Transformations Using Transformation Models and Model Finders.- Automatic Generation of Provably Correct Embedded Systems.- Complementary Methodologies for Developing Hybrid Systems with Event-B.- A Temporal Logic with Mean-Payoff Constraints.- Time Constraints with Temporal Logic Programming.- Stepwise Satisfiability Checking Procedure for Reactive System Specifications by Tableau Method and Proof System.- Equational Abstraction Refinement for Certified Tree Regular Model Checking.- SMT-Based False Positive Elimination in Static Program Analysis.- Predicate Analysis with Block-Abstraction Memoization.- Heuristic-Guided Abstraction Refinement for Concurrent Systems.- More Anti-chain Based Refinement Checking.- An Analytical and Experimental Comparison of CSP Extensions and Tools.- Symbolic Model-Checking of Stateful Timed CSP Using BDD and Digitization.- Annotations for Alloy: Automated Incremental Analysis Using Domain Specific Solvers.- State Space c-Reductions of Concurrent Systems in Rewriting Logic.- A Practical Loop Invariant Generation Approach Based on Random Testing, Constraint Solving and Verification.- ConSMutate: SQL Mutants for Guiding Concolic Testing of Database Applications.- Demonic Testing of Concurrent Programs.- Towards Certified Runtime Verification.
|
| Subject
|
:
|
Fehlertoleranz.
|
| Subject
|
:
|
Formale Methode.
|
| Subject
|
:
|
Model Checking.
|
| LC Classification
|
:
|
QA76.9.F67T674 2012
|
| Added Entry
|
:
|
Toshiaki Aoki
|
| |