The following pages link to (Q5584402):
Displaying 50 items.
- Nondeterministic semantics of compound diagrams (Q258605) (← links)
- Amorphous computing: examples, mathematics and theory (Q272778) (← links)
- Mechanizing a process algebra for network protocols (Q287372) (← links)
- Analysis of linear definite iterative loops (Q289808) (← links)
- Recent advances in program verification through computer algebra (Q351971) (← links)
- An observationally complete program logic for imperative higher-order functions (Q387994) (← links)
- On invariant checking (Q394493) (← links)
- Mechanised wire-wise verification of Handel-C synthesis (Q436367) (← links)
- Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control (Q444460) (← links)
- A survey of state vectors (Q458456) (← links)
- Certifying algorithms (Q465678) (← links)
- Verification conditions for source-level imperative programs (Q465685) (← links)
- Nonlinear invariants for linear loops and eigenpolynomials of linear operators (Q466366) (← links)
- Proving termination of nonlinear command sequences (Q470005) (← links)
- Deriving bisimulation relations from path based equivalence checkers (Q520250) (← links)
- Formal correctness proofs of a nondeterministic program (Q594577) (← links)
- The Schorr-Waite graph marking algorithm (Q599496) (← links)
- Mechanical inference of invariants for FOR-loops (Q604381) (← links)
- An elementary and unified approach to program correctness (Q607408) (← links)
- Inference of ranking functions for proving temporal properties by abstract interpretation (Q681349) (← links)
- ``A la Burstall'' intermittent assertions induction principles for proving inevitability properties of programs (Q689297) (← links)
- A new look at the automatic synthesis of linear ranking functions (Q714505) (← links)
- Proving mutual termination (Q746783) (← links)
- Constructive modal logics. I (Q750417) (← links)
- The ''Hoare logic'' of concurrent programs (Q754637) (← links)
- Semantics of algorithmic languages (Q760200) (← links)
- Synthetic programming (Q761788) (← links)
- Fair termination revisited - with delay (Q795499) (← links)
- On verification of programs with goto statements (Q801657) (← links)
- Translation and run-time validation of loop transformations (Q812060) (← links)
- Computation of equilibria in noncooperative games (Q815274) (← links)
- Decision tree learning in CEGIS-based termination analysis (Q832251) (← links)
- Generation of correctness conditions for imperative programs (Q840060) (← links)
- Proof optimization for partial redundancy elimination (Q843219) (← links)
- A method for computing the number of iterations in data dependent loops (Q853604) (← links)
- An integrated approach to high integrity software verification (Q861714) (← links)
- Towards ``dynamic domains'': totally continuous cocomplete \(\mathcal Q\)-categories (Q875519) (← links)
- A compositional natural semantics and Hoare logic for low-level languages (Q877026) (← links)
- Balancing expressiveness in formal approaches to concurrency (Q890478) (← links)
- The structure of polynomial invariants of linear loops (Q891730) (← links)
- Generating invariants for non-linear loops by linear algebraic methods (Q903492) (← links)
- A model of reconfiguration in communicating sequential processes (Q918723) (← links)
- Enabledness and termination in refinement algebra (Q923890) (← links)
- A mechanical analysis of program verification strategies (Q928673) (← links)
- Deductive verification of alternating systems (Q939163) (← links)
- Property-directed incremental invariant generation (Q939166) (← links)
- Invariants for parameterised Boolean equation systems (Q960855) (← links)
- Alternating states for dual nondeterminism in imperative programming (Q974118) (← links)
- Verifying programs by induction on their data structure: general format and applications (Q1050765) (← links)
- Process logic with regular formulas (Q1062047) (← links)
