scientific article
From MaRDI portal
Publication:2742791
zbMath0978.68033MaRDI QIDQ2742791
Robert F. Stärk, Egon Börger, Joachim Schmid
Publication date: 23 September 2001
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (37)
Verified bytecode verifiers. ⋮ Verified bytecode verification and type-certifying compilation ⋮ Concurrent abstract state machines ⋮ Neutralizing Semantic Ambiguities of Function Block Architecture by Modeling with ASM ⋮ ASM-based formal design of an adaptivity component for a cloud system ⋮ From Jinja bytecode to term rewriting: a complexity reflecting transformation ⋮ Construction and analysis of ground models and their refinements as a foundation for validating computer-based systems ⋮ Tool-assisted specification and verification of typed low-level languages ⋮ A formally verified compiler back-end ⋮ Mechanising a type-safe model of multithreaded Java with a verified compiler ⋮ An algebraic approach to the design of compilers for object-oriented languages ⋮ The rewriting logic semantics project: a progress report ⋮ The Subject-Oriented Approach to Software Design and the Abstract State Machines Method ⋮ CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types ⋮ Ambient abstract state machines with applications ⋮ Formalizing non-interference for a simple bytecode language in Coq ⋮ Towards proving type safety of .NET CIL ⋮ Towards proving type safety of \(\mathrm{C}^{\#}\) ⋮ A data-flow approach to test multi-agent ASMs ⋮ Proof-theoretic notions for software maintenance ⋮ Abstract State Machines and the Inquiry Process ⋮ An assertion-based proof system for multithreaded Java ⋮ A high-level modular definition of the semantics of C\(_{\sharp}\) ⋮ Abstract state machines: a unifying view of models of computation and of system design frameworks ⋮ Axioms for strict and lazy functional programs ⋮ An operational semantics for object-oriented concepts based on the class hierarchy ⋮ A rewriting logic approach to operational semantics ⋮ On an algorithm determining direct superclasses in Java and similar languages with inner classes-its correctness, completeness and uniqueness of solutions ⋮ A provably correct translation of the \(\lambda \)-calculus into a mathematical model of C++ ⋮ The Rewriting Logic Semantics Project: A Progress Report ⋮ A guarded fragment for abstract state machines ⋮ Formal specification and verification of the C\(\#\) thread model ⋮ A Rewriting Logic Approach to Operational Semantics (Extended Abstract) ⋮ Product optimization in stepwise design ⋮ Flashix: modular verification of a concurrent and crash-safe flash file system ⋮ Computation on structures. Behavioural theory, logic, complexity ⋮ A framework for modeling the semantics of synchronous and asynchronous procedures with abstract state machines
This page was built for publication:
