The following pages link to Formal Methods in System Design (Q169908):
Displaying 50 items.
- Mechanizing some advanced refinement concepts (Q1309250) (← links)
- Deriving correctness properties of compiled code (Q1309251) (← links)
- A formal theory of simulations between infinite automata (Q1309253) (← links)
- An embedding of timed transition systems in \(HOL\) (Q1309256) (← links)
- A proof of the nonrestoring division algorithm and its implementation on an ALU (Q1314510) (← links)
- Analysis and identification of speed-independent circuits on an event model (Q1314511) (← links)
- Newtonian arbiters cannot be proven correct (Q1314513) (← links)
- Model checking for action-based logics (Q1326587) (← links)
- An exercise in the automatic verification of asynchronous designs (Q1329086) (← links)
- Assisting requirement formalization by means of natural language translation (Q1329090) (← links)
- Gordon's computer: A hardware verification case study in OBJ3 (Q1329091) (← links)
- Rule-based induction (Q1334895) (← links)
- Constructing the real numbers in HOL (Q1334896) (← links)
- Modeling multi-rate DSP specification semantics for formal transformational design in HOL (Q1334899) (← links)
- Annotations in formal specifications and proofs (Q1334901) (← links)
- Accelerating tableaux proofs using compact representations (Q1334905) (← links)
- Property preserving abstractions for the verification of concurrent systems (Q1346649) (← links)
- A technique of state space search based on unfolding (Q1346650) (← links)
- An iterative approach to verification of real-time systems (Q1346652) (← links)
- Using integer programming to verify general safety and liveness properties (Q1346653) (← links)
- Multi-terminal binary decision diagrams (Q1355341) (← links)
- \(Mexitl\): Multimedia in executable interval temporal logic (Q1395673) (← links)
- Polynomial formal verification of multipliers (Q1395674) (← links)
- A compared study of two correctness proofs for the standardized algorithm of ABR conformance (Q1395676) (← links)
- Dynamic partitioning in linear relation analysis: application to the verification of reactive systems (Q1424999) (← links)
- An abstraction algorithm for the verification of level-sensitive latch-based netlists (Q1425001) (← links)
- Symbolic verification and analysis of discrete timed systems (Q1425003) (← links)
- A mechanized proof environment for the convenient computations proof method (Q1426938) (← links)
- Behavioral subtyping relations for active objects (Q1426939) (← links)
- Formal verification of a complex pipelined processor (Q1426941) (← links)
- An efficient partial order reduction algorithm with an alternative proviso implementation (Q1600652) (← links)
- Generating model checkers from algebraic specifications (Q1600653) (← links)
- An improvement of McMillan's unfolding algorithm (Q1600655) (← links)
- On WLCDs and the complexity of word-level decision diagrams --- A lower bound for division (Q1600657) (← links)
- Formal verification of out-of-order execution with incremental flushing (Q1604722) (← links)
- Verification of out-of-order processor designs using model Checking and a light-weight completion function (Q1604724) (← links)
- Verification of FM9801: An out-of-order microprocessor model with speculative execution, exceptions, and program-modifying capability (Q1604726) (← links)
- Special issue: Microprocessor verification (Q1606090) (← links)
- Realizability of concurrent recursive programs (Q1620953) (← links)
- An improved algorithm for the control synthesis of nonlinear sampled switched systems (Q1620955) (← links)
- Improving the results of program analysis by abstract interpretation beyond the decreasing sequence (Q1620957) (← links)
- Compact and efficiently verifiable models for concurrent systems (Q1620959) (← links)
- Special issue: program equivalence (Q1650863) (← links)
- Automating regression verification of pointer programs by predicate abstraction (Q1650864) (← links)
- Automated verification of automata communicating via FIFO and bag buffers (Q1650866) (← links)
- Algorithmic games for full ground references (Q1650867) (← links)
- Theory and methodology of assumption/commitment based system interface specification and architectural contracts (Q1654563) (← links)
- Tightening the contract refinements of a system architecture (Q1654565) (← links)
- On the complexity of monitoring Orchids signatures, and recurrence equations (Q1667643) (← links)
- Wireless protocol validation under uncertainty (Q1667647) (← links)
