The following pages link to Formal Methods in System Design (Q169908):
Displaying 50 items.
- Efficient generation of small interpolants in CNF (Q746773) (← links)
- Under-approximating loops in C programs for fast counterexample detection (Q746774) (← links)
- Extended symbolic finite automata and transducers (Q746776) (← links)
- Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists (Q746778) (← links)
- Juggrnaut: using graph grammars for abstracting unbounded heap structures (Q746781) (← links)
- Proving mutual termination (Q746783) (← links)
- CEGAR for compositional analysis of qualitative properties in Markov decision processes (Q746785) (← links)
- Automatic analysis of DMA races using model checking and \(k\)-induction (Q763238) (← links)
- On the refinement of liveness properties of distributed systems (Q763239) (← links)
- Verification of continuous dynamical systems by timed automata (Q763240) (← links)
- Network event recognition (Q812048) (← links)
- Collecting statistics over runtime executions (Q812051) (← links)
- jContractor: Introducing design-by-contract to Java using reflective bytecode instrumentation (Q812054) (← links)
- Using static analysis to reduce dynamic analysis overhead (Q812056) (← links)
- Translation and run-time validation of loop transformations (Q812060) (← links)
- Verifying time partitioning in the DEOS scheduling kernel (Q816194) (← links)
- Translating Java for multiple model checkers: The Bandera back-end (Q816196) (← links)
- Automated analysis of fault-tolerance in distributed systems (Q816197) (← links)
- Distributed symbolic model checking for \(\mu\)-calculus (Q816198) (← links)
- Formal verification of the VAMP floating point unit (Q816201) (← links)
- Stepwise development of process-algebraic specifications in decorated trace semantics (Q816202) (← links)
- Checking timed Büchi automata emptiness efficiently (Q816203) (← links)
- Reduced models for efficient CCS verification (Q816205) (← links)
- A complete mechanization of correctness of a string-preprocessing algorithm (Q816208) (← links)
- Combining symmetry reduction and under-approximation for symbolic model checking (Q816210) (← links)
- A formal framework for verification of embedded custom memories of the Motorola MPC7450 microprocessor (Q816213) (← links)
- Two case studies of semantics execution in Maude: CCS and LOTOS (Q816216) (← links)
- Formalization of fixed-point arithmetic in HOL (Q816219) (← links)
- Special issue: 20th international conference on computer aided verification (CAV'08), Princeton, NJ, USA, July 7--14, 2008. Extended versions of selected papers. (Q840635) (← links)
- Distributed synthesis for well-connected architectures (Q842581) (← links)
- Conformance testing for real-time systems (Q842583) (← links)
- Enhancing the implementation of mathematical formulas for fixed-point and floating-point arithmetics (Q845241) (← links)
- Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness (Q845242) (← links)
- Action language verifier: An infinite-state model checker for reactive software specifications (Q845244) (← links)
- Testing-based translation validation of generated code in the context of IEC 61508 (Q845246) (← links)
- Summarization for termination: No return! (Q845247) (← links)
- Why does Astrée scale up? (Q845249) (← links)
- Coverage metrics for temporal logic model checking (Q853721) (← links)
- Feature interaction detection by pairwise analysis of LTL properties -- A case study (Q853722) (← links)
- Optimistic synchronization-based state-space reduction (Q853724) (← links)
- Some ways to reduce the space dimension in polyhedra computations (Q853727) (← links)
- On using priced timed automata to achieve optimal scheduling (Q853729) (← links)
- Cones and foci: A mechanical framework for protocol verification (Q853730) (← links)
- Performance analysis of probabilistic timed automata using digital clocks (Q853731) (← links)
- Special issue: MEMOCODE 2004. Selected papers based on the presentations at the 2nd IEEE/ACM international conference on formal methods and models for co-design, San Diego, CA, USA, June 22--25, 2004. (Q854394) (← links)
- Specification and analysis of the AER/NCA active network protocol suite in real-time Maude (Q862853) (← links)
- Data structures for symbolic multi-valued model-checking (Q862857) (← links)
- Question-guided stubborn set methods for state properties (Q862861) (← links)
- Providing a formal linkage between MDG and HOL (Q878110) (← links)
- Verification of bounded Petri nets using integer programming (Q878111) (← links)