Integrated formal methods : 6th international conference, IFM 2007, Oxford, UK, July 2-5, 2007 : proceedings / / Jim Davies, Jeremy Gibbons (editors) |
Edizione | [1st ed. 2007.] |
Pubbl/distr/stampa | Berlin ; ; Heidelberg : , : Springer, , [2007] |
Descrizione fisica | 1 online resource (IX, 662 p.) |
Disciplina | 004.0151 |
Collana | Lecture notes in computer science |
Soggetto topico | Formal methods (Computer science) |
ISBN | 3-540-73210-1 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Verifying Temporal Properties of CommUnity Designs -- Precise Scenarios – A Customer-Friendly Foundation for Formal Specifications -- Automated Verification of Security Policies in Mobile Code -- Slicing Concurrent Real-Time System Specifications for Verification -- Slotted-Circus -- Bug Hunting with False Negatives -- Behavioural Specifications from Class Models -- Inheriting Laws for Processes with States -- Probabilistic Timed Behavior Trees -- Guiding the Correction of Parameterized Specifications -- Proving Linearizability Via Non-atomic Refinement -- Lifting General Correctness into Partial Correctness is ok -- Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters -- Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks -- Finding State Solutions to Temporal Logic Queries -- Qualitative Probabilistic Modelling in Event-B -- Verifying Smart Card Applications: An ASM Approach -- Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function -- UTP Semantics for Web Services -- Combining Mobility with State -- Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System -- Capturing Conflict and Confusion in CSP -- A Stepwise Development Process for Reasoning About the Reliability of Real-Time Systems -- Decomposing Integrated Specifications for Verification -- Validating Z Specifications Using the ProB Animator and Model Checker -- Verification of Multi-agent Negotiations Using the Alloy Analyzer -- Integrated Static Analysis for Linux Device Driver Verification -- Integrating Verification, Testing, and Learning for Cryptographic Protocols -- Translating FSP into LOTOS and Networks of Automata -- Common Semantics for Use Cases and Task Models -- Unifying Theories of Objects -- Non-interference Properties for Data-Type Reduction of Communicating Systems -- Co-simulation of Distributed Embedded Real-Time Control Systems. |
Record Nr. | UNISA-996465994703316 |
Berlin ; ; Heidelberg : , : Springer, , [2007] | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Integrated formal methods : 6th international conference, IFM 2007, Oxford, UK, July 2-5, 2007 : proceedings / / Jim Davies, Jeremy Gibbons (editors) |
Edizione | [1st ed. 2007.] |
Pubbl/distr/stampa | Berlin ; ; Heidelberg : , : Springer, , [2007] |
Descrizione fisica | 1 online resource (IX, 662 p.) |
Disciplina | 004.0151 |
Collana | Lecture notes in computer science |
Soggetto topico | Formal methods (Computer science) |
ISBN | 3-540-73210-1 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Verifying Temporal Properties of CommUnity Designs -- Precise Scenarios – A Customer-Friendly Foundation for Formal Specifications -- Automated Verification of Security Policies in Mobile Code -- Slicing Concurrent Real-Time System Specifications for Verification -- Slotted-Circus -- Bug Hunting with False Negatives -- Behavioural Specifications from Class Models -- Inheriting Laws for Processes with States -- Probabilistic Timed Behavior Trees -- Guiding the Correction of Parameterized Specifications -- Proving Linearizability Via Non-atomic Refinement -- Lifting General Correctness into Partial Correctness is ok -- Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters -- Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks -- Finding State Solutions to Temporal Logic Queries -- Qualitative Probabilistic Modelling in Event-B -- Verifying Smart Card Applications: An ASM Approach -- Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function -- UTP Semantics for Web Services -- Combining Mobility with State -- Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System -- Capturing Conflict and Confusion in CSP -- A Stepwise Development Process for Reasoning About the Reliability of Real-Time Systems -- Decomposing Integrated Specifications for Verification -- Validating Z Specifications Using the ProB Animator and Model Checker -- Verification of Multi-agent Negotiations Using the Alloy Analyzer -- Integrated Static Analysis for Linux Device Driver Verification -- Integrating Verification, Testing, and Learning for Cryptographic Protocols -- Translating FSP into LOTOS and Networks of Automata -- Common Semantics for Use Cases and Task Models -- Unifying Theories of Objects -- Non-interference Properties for Data-Type Reduction of Communicating Systems -- Co-simulation of Distributed Embedded Real-Time Control Systems. |
Record Nr. | UNINA-9910767515603321 |
Berlin ; ; Heidelberg : , : Springer, , [2007] | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Teaching formal methods : second international conference, TFM 2009, Eindhoven, the Netherlands, November 2-6, 2009 : proceedings / / Jeremy Gibbons, Jos Nuno Oliveira (Eds.) |
Edizione | [1st ed. 2009.] |
Pubbl/distr/stampa | Berlin ; ; New York, : Springer, c2009 |
Descrizione fisica | 1 online resource (XI, 177 p.) |
Disciplina | 004n/a |
Altri autori (Persone) |
GibbonsJeremy <1966->
OliveiraJos N |
Collana |
Lecture notes in computer science
LNCS sublibrary. SL 1, Theoretical computer science and general issues |
Soggetto topico |
Formal methods (Computer science)
Computer software - Development - Study and teaching |
ISBN | 3-642-04912-5 |
Classificazione |
DAT 310f
EDU 740f SS 4800 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Abstraction and Modelling: A Complementary Partnership -- Teaching Formal Methods for the Unconquered Territory -- Teaching Formal Methods Based on Rewriting Logic and Maude -- Which Mathematics for the Information Society? -- What Top-Level Software Engineers Tackle after Learning Formal Methods: Experiences from the Top SE Project -- Chief Chefs of Z to Alloy: Using a Kitchen Example to Teach Alloy with Z -- Teaching Program Specification and Verification Using JML and ESC/Java2 -- How to Explain Mistakes -- Integrated and Tool-Supported Teaching of Testing, Debugging, and Verification -- On Teaching Formal Methods: Behavior Models and Code Analysis -- Teaching Concurrency: Theory in Practice. |
Altri titoli varianti | TFM 2009 |
Record Nr. | UNINA-9910484293203321 |
Berlin ; ; New York, : Springer, c2009 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|