scientific article; zbMATH DE number 3574936

From MaRDI portal
Publication:4144755

zbMath0368.68005MaRDI QIDQ4144755

Edsger W. Dijkstra

Publication date: 1976


Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.



Related Items (only showing first 100 items - show all)

Specification and initialization of a logic computer systemDistributed termination on a ringA formalization of programs in first-order logic with a discrete linear orderGuard modulesA context dependent equivalence between processesGeneration of correctness conditions for imperative programsThe formal development of a parallel program performing LU-decompositionMechanical translation of set theoretic problem specifications into efficient RAM code - a case studyAngelic nondeterminism in the unifying theories of programmingTank monitoring: A pAMN case studyThe specification logic \(\nu \)ZCompiling communicating processes into delay-insensitive VLSI circuitsFairness and the axioms of control predicatesA sharp proof rule for procedures in WP semanticsSynthesis of large dynamic concurrent programs from dynamic specificationsA calculus of refinements for program derivations\textit{Theorema}: Towards computer-aided mathematical theory explorationLattice-valued topological systems as a framework for lattice-valued formal concept analysisProcedure mechanisms of abstractionThe Schorr-Waite graph marking algorithmThe \(\mu\)-calculus as an assertion-language for fairness argumentsReflexive transitive invariant relations: A basis for computing loop functionsModular inference of subprogram contracts for safety checkingFlow analysis of lazy higher-order functional programsPolyhedral approximations of strictly convex compactaAn algebraic approach to the design of compilers for object-oriented languagesAn elementary and unified approach to program correctnessParameter passing in nondeterministic recursive programsAutomated flaw detection in algebraic specificationsLattice-valued soft algebras.Orthogonality of information structuresAgent planning programsGenerating invariants for non-linear loops by linear algebraic methodsApplication of modal logic to programmingUna teoria algebrica per i guarded commands di DijkstraA functional framework for agent-based models of exchangeDoomed program pointsA proof technique for communicating sequential processesCompositional refinement in agent-based security protocolsInvariant diagrams with data refinementMechanised support for sound refinement tacticsCompositional noninterference from first principlesExperiments in program verification using Event-BAnother look at the longest ascending subsequence problemMechanical reasoning about families of UTP theoriesAssurance of dynamic adaptation in distributed systemsA simple relation between relational and predicate transformer semantics for nondeterministic programsDo-it-yourself type theoryCommand algebras, recursion and program transformationA programming model for BSP with partitioned synchronisationInvariants in the application-oriented specification of control systemsRefinement concepts formalised in higher order logicDerivation of efficient parallel programs: An example from genetic sequence analysisProof obligations for blocks and proceduresThe shadow knows: refinement and security in sequential programsEnabledness and termination in refinement algebraVerification conditions for source-level imperative programsReasoning about orchestrations of web services using partial correctnessDeriving dense linear algebra librariesVerification of evolving software via component substitutability analysisAlgebraic reasoning for probabilistic action systems and while-loopsModelling higher-order dual nondeterminacyA single complete rule for data refinementAsynchronous datapaths and the design of an asynchronous adderLogical foundations for programming semanticsAcquiring search-control knowledge via static analysisAdas and the equational theory of if-then-elseDual choice and iteration in an abstract algebra of actionOn the purpose of Event-B proof obligationsA process algebraic framework for specification and validation of real-time systemsCompleteness of fair ASM refinementCompetent predicate abstraction in model checkingHoare logic-based genetic programmingAlgebraic separation logicChanging system interfaces consistently: a new refinement strategy for CSP\(\|\)BQuantum loop programsTransforming semantics by abstract interpretationA new taxonomy of sublinear right-to-left scanning keyword pattern matching algorithmsMining early aspects based on syntactical and dependency analysesAn axiomatic treatment of SIMD assignmentGeneralised quantum weakest preconditionsDual unbounded nondeterminacy, recursion, and fixpointsTest-data generation for control coverage by proofProvably correct derivation of algorithms using FermaTA UTP semantics for \textsf{Circus}Invariant based programming: Basic approach and teaching experiencesA comparison of tools for teaching formal software verificationSynthetic programmingCorrect hardware synthesisLocal proofs for global safety propertiesMathematics for reasoning about loop functionsA logic covering undefinedness in program proofsAn algebraic approach to the syntax and semantics of languages with subscripted variablesNon-deterministic data types: Models and implementationsThe axiomatic semantics of programs based on Hoare's logicA model of concurrency with fair merge and full recursionComputation of equilibria in noncooperative gamesNondeterministic semantics of compound diagramsStepwise development of process-algebraic specifications in decorated trace semanticsA simple fixpoint argument without the restriction to continuity




This page was built for publication: