Formal Methods and Software Engineering 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14-15, 2007. Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Butler, Michael (Επιμελητής έκδοσης), Hinchey, Michael G. (Επιμελητής έκδοσης), Larrondo-Petrie, María M. (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2007.
• Σειρά: Lecture Notes in Computer Science, 4789
• Θέματα: Computer science.; Software engineering.; Computer programming.; Programming languages (Electronic computers).; Computer logic.; Computers.; Computer Science.; Software Engineering/Programming and Operating Systems.; Programming Techniques.; Software Engineering.; Models and Principles.; Logics and Meanings of Programs.; Programming Languages, Compilers, Interpreters.

Πίνακας περιεχομένων:

• Invited Talks
• A System Development Process with Event-B and the Rodin Platform
• Challenges in Software Certification
• Security and Knowledge
• Integrating Formal Methods with System Management
• Formal Engineering of XACML Access Control Policies in VDM++
• A Verification Framework for Agent Knowledge
• Embedded Systems
• From Model-Based Design to Formal Verification of Adaptive Embedded Systems
• Machine-Assisted Proof Support for Validation Beyond Simulink
• VeSTA: A Tool to Verify the Correct Integration of a Component in a Composite Timed System
• Testing
• Integrating Specification-Based Review and Testing for Detecting Errors in Programs
• Testing for Refinement in CSP
• Reducing Test Sequence Length Using Invertible Sequences
• Automated Analysis
• Model Checking with SAT-Based Characterization of ACTL Formulas
• Automating Refinement Checking in Probabilistic System Design
• Model Checking in Practice: Analysis of Generic Bootloader Using SPIN
• Model Checking Propositional Projection Temporal Logic Based on SPIN
• Hardware
• A Denotational Semantics for Handel-C Hardware Compilation
• Automatic Generation of Verified Concurrent Hardware
• Modeling and Verification of Master/Slave Clock Synchronization Using Hybrid Automata and Model-Checking
• Concurrency
• Efficient Symbolic Execution of Large Quantifications in a Process Algebra
• Formalizing SANE Virtual Processor in Thread Algebra
• Calculating and Composing Progress Properties in Terms of the Leads-to Relation
• Erratum
• Erratum to: Challenges in Software Certification.