The following pages link to Formal Methods in System Design (Q169908):
Displaying 50 items.
- Causality problem in real-time calculus (Q346787) (← links)
- Decentralised LTL monitoring (Q346789) (← links)
- Synthesis of large dynamic concurrent programs from dynamic specifications (Q346790) (← links)
- Special issue: Computer aided verification (CAV'09). Selected papers based on the presentations at the 21st conference, Grenoble, France, June 26 -- July 2, 2009 (Q420532) (← links)
- Special issue: Computer aided verification (CAV'10). Selected papers based on the presentations at the 22nd international conference, Edinburgh, UK, July 15--19, 2010. (Q420533) (← links)
- Feasibility analysis for robustness quantification by symbolic model checking (Q453480) (← links)
- Benchmarking a model checker for algorithmic improvements and tuning for performance (Q453484) (← links)
- Incremental preprocessing methods for use in BMC (Q453488) (← links)
- Specification and encoding of transaction interaction properties (Q453491) (← links)
- Exploring structural symmetry automatically in symbolic trajectory evaluation (Q453494) (← links)
- Antichains and compositional algorithms for LTL synthesis (Q453498) (← links)
- Priority scheduling of distributed systems based on model checking (Q453501) (← links)
- Cuts from proofs: a complete and practical technique for solving linear inequalities over integers (Q453505) (← links)
- Verification of STM on relaxed memory models (Q453508) (← links)
- Synthesis of opaque systems with static and dynamic masks (Q453510) (← links)
- Interrupt timed automata: verification and expressiveness (Q453513) (← links)
- Explaining counterexamples using causality (Q453516) (← links)
- Transparent partial order reduction (Q453518) (← links)
- Efficient emptiness check for timed Büchi automata (Q453519) (← links)
- Fences in weak memory models (Q453523) (← links)
- Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics (Q453526) (← links)
- Achieving distributed control through model checking (Q453529) (← links)
- Bounded underapproximations (Q453533) (← links)
- Symbolic bounded synthesis (Q453535) (← links)
- Constructive Boolean circuits and the exactness of timed ternary simulation (Q453539) (← links)
- A concurrency-preserving translation from time Petri nets to networks of timed automata (Q453542) (← links)
- Bisimulation and simulation algorithms on probabilistic transition systems by abstract interpretation (Q453545) (← links)
- Runtime verification of embedded real-time systems (Q479806) (← links)
- A modal characterization of alternating approximate bisimilarity (Q479808) (← links)
- Hardness and inapproximability of minimizing adaptive distinguishing sequences (Q479811) (← links)
- Resolution proof transformation for compression and interpolation (Q479815) (← links)
- SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata (Q479819) (← links)
- An extension of lazy abstraction with interpolation for programs with arrays (Q479820) (← links)
- Quantifier elimination by dependency sequents (Q479823) (← links)
- Quantifier-free encoding of invariants for hybrid systems (Q479826) (← links)
- Verification of Galois field based circuits by formal reasoning based on computational algebraic geometry (Q479832) (← links)
- Deciding floating-point logic with abstract conflict driven clause learning (Q479837) (← links)
- Verifying global start-up for a Möbius ring-oscillator (Q479839) (← links)
- Budget-bounded model-checking pushdown systems (Q479843) (← links)
- Finite controlled invariants for sampled switched systems (Q487251) (← links)
- On regions and zones for event-clock automata (Q487253) (← links)
- Runtime enforcement of timed properties revisited (Q487258) (← links)
- The spirit of ghost code (Q518394) (← links)
- SMT-based model checking for recursive programs (Q518396) (← links)
- An efficient SMT solver for string constraints (Q518402) (← links)
- From invariant checking to invariant inference using randomized search (Q518404) (← links)
- A search-based procedure for nonlinear real arithmetic (Q518407) (← links)
- Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components (Q518409) (← links)
- Reachability computation for polynomial dynamical systems (Q526433) (← links)
- SAT solver management strategies in IC3: an experimental approach (Q526434) (← links)
