Formal Methods and Software Engineering
Springer Berlin (Verlag)
978-3-642-34280-6 (ISBN)
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-Order
Logic.- 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.
Erscheint lt. Verlag | 19.9.2012 |
---|---|
Reihe/Serie | Lecture Notes in Computer Science | Programming and Software Engineering |
Zusatzinfo | XIV, 512 p. 131 illus. |
Verlagsort | Berlin |
Sprache | englisch |
Maße | 155 x 235 mm |
Gewicht | 789 g |
Themenwelt | Mathematik / Informatik ► Informatik ► Netzwerke |
Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge | |
Mathematik / Informatik ► Informatik ► Software Entwicklung | |
Informatik ► Theorie / Studium ► Algorithmen | |
Schlagworte | Algorithm analysis and problem complexity • Concurrent Systems • Distributed Systems • Model Checking • specification optimization • temporal logic |
ISBN-10 | 3-642-34280-9 / 3642342809 |
ISBN-13 | 978-3-642-34280-6 / 9783642342806 |
Zustand | Neuware |
Haben Sie eine Frage zum Produkt? |
aus dem Bereich