Theory and Practice of Formal Methods

Theory and Practice of Formal Methods

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

Bonsangue, Marcello; Abraham, Erika; Johnsen, Einar Broch

Springer International Publishing AG

03/2016

427

Mole

Inglês

9783319307336

15 a 20 dias

6613

Descrição não disponível.
Program Verification: to Err is
Human.-
Fond (and Frank) Memories of Frank.- Warmest Congratulations, Frank.- Conformance
Checking of Real-Time Models: Symbolic Execution vs. Bounded Model Checking.- Resource
Analysis of Distributed Systems.- Comparing Trace Expressions and Linear
Temporal Logic for Runtime Verification.- Proper Protocol.- A Compositional
Approach to the Verification of Hybrid Systems.- Array Abstraction with
Symbolic Pivots.- Modeling Role-Based Systems with Exogenous Coordination.- Vats:
A Safe, Reactive Storage Abstraction.- Denotational and Operational Preciseness
of Subtyping: A Roadmap.- A Sound and Complete Hoare Logic for
Dynamically-Typed, Object-Oriented Programs.- Self-Reconfiguring
Microservices.- Statically and Dynamically Verifiable SLA metrics.- Effectively
Eliminating Auxiliaries.- Towards a Proof Method for Paradigm.- Toward a Formal
Foundation for Time Travel in Stories and Games.- Industrial Application of
Formal Models Generated from Domain SpecificLanguages.- Formal Verification of
Open Normative Multi-Agent System.- Moessner's Theorem: An Exercise in Coinductive
Reasoning in Coq.- Towards a Kool Future.- On the Expressiveness of Synchronization
in Component Deployment.- Characterisation of Simulation by Probabilistic
Testing.- On Time Actors.- A Small-Step Semantics of a Concurrent Calculus with
Goroutines and Deferred Functions.- Quicksort Revisited - Verifying Alternative
Versions of Quicksort.
Este título pertence ao(s) assunto(s) indicados(s). Para ver outros títulos clique no assunto desejado.
abstract interpretation;algorithms;axiomatic semantics;program transformation and verification;runtime verification;actor model;array abstraction;automated verification;completeness for total correctness;dynamic typing;loop invariant generation;microservices;multiple notions of correctness;pure object-orientation;quicksort;reduction technique;relative completeness;service-oriented architecture;soundness;tagged hoare logic