ENTCS
2007
13 years 6 months ago
2007
ENTCS
2007
13 years 6 months ago
2007
The need for backward execution in debuggers has been raised a number of times. Backward execution helps a user naturally think backwards and, in turn, easily locate the cause of ...
ENTCS
2007
13 years 6 months ago
2007
Modern integrated development environments (IDEs) provide programmers with a variety of sophisticated tools for program visualization and manipulation. These tools assist the prog...
ENTCS
2007
13 years 6 months ago
2007
If a program does not fulfill a given specification, a model checker delivers a counterexample, a run which demonstrates the wrong behavior. Even with a counterexample, locating...
ENTCS
2007
13 years 6 months ago
2007
We present a syntactic scheme for translating future-time LTL bounded model checking problems into propositional satisfiability problems. The scheme is similar in principle to th...
ENTCS
2007
13 years 6 months ago
2007
Bounded Model Checking (BMC) is one of the most paradigmatic practical applications of Boolean Satisfiability (SAT). The utilization of SAT in model checking has allowed signifi...
ENTCS
2007
13 years 6 months ago
2007
We consider the non-orthodox proof rules of hybrid logic from the viewpoint of topological semantics. Topological semantics is more general than Kripke semantics. We show that the...
ENTCS
2007
13 years 6 months ago
2007
This article describes an architecture for creating responsive web interfaces for proof assistants. The architecture combines current web development technologies with the functio...
ENTCS
2007
13 years 6 months ago
2007
Nominal rewriting introduced a novel method of specifying rewriting on syntax-with-binding. We extend this treatment of rewriting with hierarchy of variables representing increasi...
ENTCS
2007
13 years 6 months ago
2007
We describe how a set-theoretic foundation for mathematics can be encoded in the new system Scunak. We then discuss an encoding of the construction of functions as functional relat...