scientific article; zbMATH DE number 3574936
From MaRDI portal
Publication:4144755
zbMath0368.68005MaRDI QIDQ4144755
Publication date: 1976
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Research exposition (monographs, survey articles) pertaining to computer science (68-02) General topics in the theory of software (68N01)
Related Items (only showing first 100 items - show all)
Specification and initialization of a logic computer system ⋮ Distributed termination on a ring ⋮ A formalization of programs in first-order logic with a discrete linear order ⋮ Guard modules ⋮ A context dependent equivalence between processes ⋮ Generation of correctness conditions for imperative programs ⋮ The formal development of a parallel program performing LU-decomposition ⋮ Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study ⋮ Angelic nondeterminism in the unifying theories of programming ⋮ Tank monitoring: A pAMN case study ⋮ The specification logic \(\nu \)Z ⋮ Compiling communicating processes into delay-insensitive VLSI circuits ⋮ Fairness and the axioms of control predicates ⋮ A sharp proof rule for procedures in WP semantics ⋮ Synthesis of large dynamic concurrent programs from dynamic specifications ⋮ A calculus of refinements for program derivations ⋮ \textit{Theorema}: Towards computer-aided mathematical theory exploration ⋮ Lattice-valued topological systems as a framework for lattice-valued formal concept analysis ⋮ Procedure mechanisms of abstraction ⋮ The Schorr-Waite graph marking algorithm ⋮ The \(\mu\)-calculus as an assertion-language for fairness arguments ⋮ Reflexive transitive invariant relations: A basis for computing loop functions ⋮ Modular inference of subprogram contracts for safety checking ⋮ Flow analysis of lazy higher-order functional programs ⋮ Polyhedral approximations of strictly convex compacta ⋮ An algebraic approach to the design of compilers for object-oriented languages ⋮ An elementary and unified approach to program correctness ⋮ Parameter passing in nondeterministic recursive programs ⋮ Automated flaw detection in algebraic specifications ⋮ Lattice-valued soft algebras. ⋮ Orthogonality of information structures ⋮ Agent planning programs ⋮ Generating invariants for non-linear loops by linear algebraic methods ⋮ Application of modal logic to programming ⋮ Una teoria algebrica per i guarded commands di Dijkstra ⋮ A functional framework for agent-based models of exchange ⋮ Doomed program points ⋮ A proof technique for communicating sequential processes ⋮ Compositional refinement in agent-based security protocols ⋮ Invariant diagrams with data refinement ⋮ Mechanised support for sound refinement tactics ⋮ Compositional noninterference from first principles ⋮ Experiments in program verification using Event-B ⋮ Another look at the longest ascending subsequence problem ⋮ Mechanical reasoning about families of UTP theories ⋮ Assurance of dynamic adaptation in distributed systems ⋮ A simple relation between relational and predicate transformer semantics for nondeterministic programs ⋮ Do-it-yourself type theory ⋮ Command algebras, recursion and program transformation ⋮ A programming model for BSP with partitioned synchronisation ⋮ Invariants in the application-oriented specification of control systems ⋮ Refinement concepts formalised in higher order logic ⋮ Derivation of efficient parallel programs: An example from genetic sequence analysis ⋮ Proof obligations for blocks and procedures ⋮ The shadow knows: refinement and security in sequential programs ⋮ Enabledness and termination in refinement algebra ⋮ Verification conditions for source-level imperative programs ⋮ Reasoning about orchestrations of web services using partial correctness ⋮ Deriving dense linear algebra libraries ⋮ Verification of evolving software via component substitutability analysis ⋮ Algebraic reasoning for probabilistic action systems and while-loops ⋮ Modelling higher-order dual nondeterminacy ⋮ A single complete rule for data refinement ⋮ Asynchronous datapaths and the design of an asynchronous adder ⋮ Logical foundations for programming semantics ⋮ Acquiring search-control knowledge via static analysis ⋮ Adas and the equational theory of if-then-else ⋮ Dual choice and iteration in an abstract algebra of action ⋮ On the purpose of Event-B proof obligations ⋮ A process algebraic framework for specification and validation of real-time systems ⋮ Completeness of fair ASM refinement ⋮ Competent predicate abstraction in model checking ⋮ Hoare logic-based genetic programming ⋮ Algebraic separation logic ⋮ Changing system interfaces consistently: a new refinement strategy for CSP\(\|\)B ⋮ Quantum loop programs ⋮ Transforming semantics by abstract interpretation ⋮ A new taxonomy of sublinear right-to-left scanning keyword pattern matching algorithms ⋮ Mining early aspects based on syntactical and dependency analyses ⋮ An axiomatic treatment of SIMD assignment ⋮ Generalised quantum weakest preconditions ⋮ Dual unbounded nondeterminacy, recursion, and fixpoints ⋮ Test-data generation for control coverage by proof ⋮ Provably correct derivation of algorithms using FermaT ⋮ A UTP semantics for \textsf{Circus} ⋮ Invariant based programming: Basic approach and teaching experiences ⋮ A comparison of tools for teaching formal software verification ⋮ Synthetic programming ⋮ Correct hardware synthesis ⋮ Local proofs for global safety properties ⋮ Mathematics for reasoning about loop functions ⋮ A logic covering undefinedness in program proofs ⋮ An algebraic approach to the syntax and semantics of languages with subscripted variables ⋮ Non-deterministic data types: Models and implementations ⋮ The axiomatic semantics of programs based on Hoare's logic ⋮ A model of concurrency with fair merge and full recursion ⋮ Computation of equilibria in noncooperative games ⋮ Nondeterministic semantics of compound diagrams ⋮ Stepwise development of process-algebraic specifications in decorated trace semantics ⋮ A simple fixpoint argument without the restriction to continuity
This page was built for publication: