enter search term and/or author name
A game-based framework for CTL counterexamples and 3-valued abstraction-refinement
Sharon Shoham, Orna Grumberg
Article No.: 1
This work exploits and extends the game-based framework of CTL model checking for counterexample and incremental abstraction-refinement. We define a game-based CTL model checking for abstract models over the 3-valued semantics, which can be used...
A formally verified proof of the prime number theorem
Jeremy Avigad, Kevin Donnelly, David Gray, Paul Raff
Article No.: 2
The prime number theorem, established by Hadamard and de la Vallée Poussin independently in 1896, asserts that the density of primes in the positive integers is asymptotic to 1/ln x. Whereas their proofs made serious use of the...
Polymorphic type inference for the named nested relational calculus
Jan Van den Bussche, Stijn Vansummeren
Article No.: 3
The named nested relational calculus is the canonical query language for the complex object database model and is equipped with a natural static type system. Given an expression in the language, without type declarations for the input variables,...
Predicate abstraction provides a powerful tool for verifying properties of infinite-state systems using a combination of a decision procedure for a subset of first-order logic and symbolic methods originally developed for finite-state model...
Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties
Christel Baier, Nathalie Bertrand, Philippe Schnoebelen
Article No.: 5
Lossy channel systems (LCS's) are systems of finite state processes that communicate via unreliable unbounded fifo channels. We introduce NPLCS's, a variant of LCS's where message losses have a probabilistic behavior while the component processes...
We materialize the common understanding that calculi with explicit substitutions provide an intermediate step between an abstract specification of substitution in the lambda-calculus and its concrete implementations. To this end, we go back to...
The development of effective knowledge discovery techniques has become a very active research area in recent years due to the important impact it has had in several relevant application domains. One interesting task therein is that of singling out...