LOIS
Looping Over Infinite Sets
Eryk Kopczyński, Szymon Toruńczyk
Papers and technical documentation
LOIS: technical documentation. PDF (Feb 1, 2016)
Abstract:
LOIS is a C++ library allowing iterating through certain infinite sets, in finite time.
The resulting language has an intuitive semantics,
corresponding to execution of infinitely
many threads in parallel.
This allows to merge the power of abstract mathematical constructions
into imperative programming.
Infinite sets are internally represented
using first order formulas over some underlying logical structure.
To effectively handle such sets, we use and implement SMT solvers for various first order
theories. LOIS has applications in education, and in verification of infinite state systems.
This is a technical documentation of LOIS, describing how to write programs using it.
LOIS: syntax and semantics. PDF (Oct 6, 2016) (accepted to POPL 2017)
Abstract:
We present the semantics of a programming language called LOIS, which allows iterating
through certain infinite sets, in finite time. Our semantics intuitively
correspond to execution of infinitely many threads in parallel.
This allows to merge the power of abstract mathematical constructions
into imperative programming.
Infinite sets are internally represented
using first order formulas over some underlying logical structure.
LOIS: an application of SMT solvers. PDF (Apr 25, 2016) (accepted to SMT 2016)
Abstract:
We present an implemented programming language called LOIS,
which allows iterating through certain infinite sets,
in finite time. We demonstrate how this language
offers a new application of SMT solvers to theoretical verification, by showing that many known problems concerning infinite-state systems can easily be implemented using LOIS, which in turn invokes SMT solvers
for an underlying theory.
In many applications, ω-categorical theories
with quantifier elimination are of particular
interest.
Our tests indicate that state-of-the art solvers perform poorly on such theories, as they are outperformed by
orders of magnitude by a simple quantifier-elimination procedure.
Public repository
NEW (since Oct 13, 2016): the ongoing development of LOIS is hosted on GitHub here.
Prototypes
- lois.tgz (Oct 6, 2016)
The current prototype of LOIS. Includes source code (LOIS library itself, examples from the paper, and an automatic testing program, Makefile).
Installation and testing:
- You need tar, gcc (supporting the C++11 standard), and make. Those are very standard tools under Unix-like environments.
- Extract the package: tar zxf lois.tgz
- Enter the lois directory created: cd lois
- Run make: make
This should compile the LOIS library and
several included test programs using it (tutorial -- examples from the papers, autotest --
automatic testing program, and mintest -- automata minimization),
run the test programs, and put their output in the subdirectory out.
Consult the technical documentation above (section Tutorial) to learn how to use LOIS for your own purposes.
If you want to test LOIS with the SMT solvers:
- Install the solvers
- Edit tests/soltest.cpp -- you will probably want to
adapt the commandlines in function testSolvers to conform with your installation.
- Run make out/soltest.txt -- the results will be saved in files out/sol*.txt.
- lois-results.tgz (Oct 6, 2016)
The current prototype of LOIS, and results.
Also includes the result of make (both binaries and their output).
- solver-tests.tgz (May 1, 2016)
Details about the solvers used, and the results of our tests.
The generated queries (smt-lib 2 format, incremental) are included.
Note: we have checked recently that the newest version of CVC4 works much better
than the one we have tested in May -- all queries are now answered in reasonable time,
yet still a bit slower than internal. (However, Z3 still has problems.)
Also the time is incorrectly said to be given in milliseconds, while it is actually
in microseconds.
LOIS is released under the MIT license. It has been tested under:
- gcc version 4.4.3, i686 architecture
- gcc version 4,6.3, x86_64 architecture
- gcc version 4.7.3, x86_64 architecture
- gcc version 4,9.4, x86_64 architecture
