Theory and Practice of Formal Methods

Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday

AvErika Ábrahám,Marcello Bonsangue

Häftad, Engelska, 2016

Del 9660 i serien Lecture Notes in Computer Science

556 kr

Beställningsvara. Skickas inom 10-15 vardagar. Fri frakt över 249 kr.

Beskrivning

This Festschrift volume has been published in honor ofFrank de Boer, on the occasion of his 60th birthday. Frank S. For a while, he also liked failures, especially in semantics, andoptimistically concluded with the failure of failures.

Produktinformation

Utgivningsdatum:2016-03-13
Mått:155 x 235 x 24 mm
Vikt:663 g
Format:Häftad
Språk:Engelska
Serie:Lecture Notes in Computer Science
Antal sidor:427
Förlag:Springer International Publishing AG
ISBN:9783319307336

Utforska kategorier

Innehållsförteckning

Program Verification: to Err isHuman.-Fond (and Frank) Memories of Frank.- Warmest Congratulations, Frank.- ConformanceChecking of Real-Time Models: Symbolic Execution vs. Bounded Model Checking.- ResourceAnalysis of Distributed Systems.- Comparing Trace Expressions and LinearTemporal Logic for Runtime Verification.- Proper Protocol.- A CompositionalApproach to the Verification of Hybrid Systems.- Array Abstraction withSymbolic Pivots.- Modeling Role-Based Systems with Exogenous Coordination.- Vats:A Safe, Reactive Storage Abstraction.- Denotational and Operational Precisenessof Subtyping: A Roadmap.- A Sound and Complete Hoare Logic forDynamically-Typed, Object-Oriented Programs.- Self-ReconfiguringMicroservices.- Statically and Dynamically Verifiable SLA metrics.- EffectivelyEliminating Auxiliaries.- Towards a Proof Method for Paradigm.- Toward a FormalFoundation for Time Travel in Stories and Games.- Industrial Application ofFormal Models Generated from Domain SpecificLanguages.- Formal Verification ofOpen Normative Multi-Agent System.- Moessner’s Theorem: An Exercise in CoinductiveReasoning in Coq.- Towards a Kool Future.- On the Expressiveness of Synchronizationin Component Deployment.- Characterisation of Simulation by ProbabilisticTesting.- On Time Actors.- A Small-Step Semantics of a Concurrent Calculus withGoroutines and Deferred Functions.- Quicksort Revisited - Verifying AlternativeVersions of Quicksort.