Theory and Practice of Formal Methods
Springer International Publishing (Verlag)
978-3-319-30733-6 (ISBN)
This Festschrift volume has been published in honor ofFrank de Boer, on the occasion of his 60th birthday.
Frank S. de Boer is a prominent member of the research community in formalmethods and theoretical computer science. A brief look at his lengthypublication list reveals a broad area of interest and a versatile modusoperandi with: logic and constraint programming; deductive proof systems,soundness, and completeness; semantics, compositionality, and full abstraction;process algebra and decidability; multithreading and actor-based concurrency;agent programming, ontologies, and modal logic; real-time systems, timedautomata, and schedulability; enterprise architectures, choreography, andcoordination; testing and runtime monitoring; and cloud computing and service-levelagreements. For a while, he also liked failures, especially in semantics, andoptimistically concluded with the failure of failures. In fact, Frank has anopportunistic approach to research. Rather than seeing obstacles, he findsopportunities.
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.
| Erscheinungsdatum | 08.10.2016 |
|---|---|
| Reihe/Serie | Lecture Notes in Computer Science | Theoretical Computer Science and General Issues |
| Zusatzinfo | XII, 427 p. 112 illus. in color. |
| Verlagsort | Cham |
| Sprache | englisch |
| Maße | 155 x 235 mm |
| Themenwelt | Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge |
| Mathematik / Informatik ► Informatik ► Software Entwicklung | |
| Informatik ► Theorie / Studium ► Algorithmen | |
| Informatik ► Theorie / Studium ► Künstliche Intelligenz / Robotik | |
| Schlagworte | Abstract Interpretation • Actor Model • Algorithm analysis and problem complexity • algorithms • array abstraction • artificial intelligence (incl. robotics) • Automated Verification • axiomatic semantics • completeness for total correctness • dynamic typing • Logics and meanings of programs • loop invariant generation • Mathematical logic and formal languages • Microservices • multiple notions of correctness • Programming languages, compilers, interpreters • program transformation and verification • pure object-orientation • Quicksort • reduction technique • relative completeness • runtime verification • Service-Oriented Architecture • Software engineering • Software Engineering / Softwareentwicklung • soundness • tagged hoare logic |
| ISBN-10 | 3-319-30733-9 / 3319307339 |
| ISBN-13 | 978-3-319-30733-6 / 9783319307336 |
| Zustand | Neuware |
| Haben Sie eine Frage zum Produkt? |
aus dem Bereich
