東華大學圖書館 |

Formal methods and software engineering = 14th international conference on formal engineering methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012 : proceedings /

紀錄類型:	書目-電子資源 : Monograph/item
正題名/作者:	Formal methods and software engineering/ edited by Toshiaki Aoki, Kenji Taguchi.
其他題名:	14th international conference on formal engineering methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012 : proceedings /
其他作者:	Aoki, Toshiaki.
出版者:	Berlin, Heidelberg :Springer Berlin Heidelberg : : 2012.,
面頁冊數:	xiv, 512 p. :ill., digital ;24 cm.
內容註:	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.
Contained By:	Springer eBooks
標題:	Formal methods (Computer science) -
電子資源:	http://dx.doi.org/10.1007/978-3-642-34281-3
ISBN:	9783642342813 (electronic bk.)

Formal methods and software engineering = 14th international conference on formal engineering methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012 : proceedings /
Formal methods and software engineering14th international conference on formal engineering methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012 : proceedings /[electronic resource] :edited by Toshiaki Aoki, Kenji Taguchi. - Berlin, Heidelberg :Springer Berlin Heidelberg :2012. - xiv, 512 p. :ill., digital ;24 cm. - Lecture notes in computer science,76350302-9743 ;. - Lecture notes in computer science ;5353..

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.

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.

ISBN: 9783642342813 (electronic bk.)Subjects--Topical Terms:

882407
Formal methods (Computer science)

LC Class. No.: QA76.9.F67 / I5788 2012

Dewey Class. No.: 005.1

Formal methods and software engineering = 14th international conference on formal engineering methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012 : proceedings /
LDR:04084nmm a2200289 a 4500 001 1329260
003 DE-He213
005 20121123094010.0
006 m d
007 cr nn 008maaau
008 130207s2012 gw s 0 eng d
020 $a 9783642342813 (electronic bk.)
020 $a 9783642342806 (paper)
035 $a 978-3-642-34281-3
040 $a GP $c GP
041 0 $a eng
050 4 $a QA76.9.F67 $b I5788 2012
082 0 4 $a 005.1 $2 23
090 $a QA76.9.F67 $b I61 2012
245 1 0 $a Formal methods and software engineering $h [electronic resource] : $b 14th international conference on formal engineering methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012 : proceedings / $c edited by Toshiaki Aoki, Kenji Taguchi.
260 $a Berlin, Heidelberg : $b Springer Berlin Heidelberg : $b Imprint: Springer, $c 2012.
300 $a xiv, 512 p. : $b ill., digital ; $c 24 cm.
490 1 $a Lecture notes in computer science, $x 0302-9743 ; $v 7635
505 0 $a 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.
520 $a 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.
650 0 $a Formal methods (Computer science) $3 882407
650 0 $a Software engineering $v Congresses. $3 1243492
650 0 $a Computer software $x Verification $v Congresses. $3 1244120
650 1 4 $a Computer Science. $3 626642
650 2 4 $a Software Engineering. $3 890874
650 2 4 $a Programming Techniques. $3 892496
650 2 4 $a Programming Languages, Compilers, Interpreters. $3 891123
650 2 4 $a Algorithm Analysis and Problem Complexity. $3 891007
650 2 4 $a Mathematical Logic and Formal Languages. $3 892517
650 2 4 $a Computer Communication Networks. $3 775497
700 1 $a Aoki, Toshiaki. $3 1620979
700 1 $a Taguchi, Kenji. $3 1620980
710 2 $a SpringerLink (Online service) $3 836513
773 0 $t Springer eBooks
830 0 $a Lecture notes in computer science ; $v 5353. $x 0302-9743 $3 1274248
856 4 0 $u http://dx.doi.org/10.1007/978-3-642-34281-3
950 $a Computer Science (Springer-11645)