|
ResQu
News
- 2011-07: Version 0.1 released
- 2013-05: Version 1.0 released (now also works with QRP)
- 2014-05: Version 2.0 released (can perform certificate minimization)
- 2015-01: Version LP released (works with LQ resolution proofs)
Description
- ResQu is a tool for deriving Herbrand/Skolem functions from Q-resolution and Q-consensus proofs.
- Input formats:
- QBC (proof formats of Squolem, EBDDRES);
- Proof format of Qube-cert;
- QRP (Proof format of cDepQBF);
- RFAO (local input format as a right-firat-and-or formula just for certificate optimization)
- Output formats: BLIF (format of ABC synthesis tool), RFAO (same as above)
Link
ResQu
|
| |
Software Workaround Benchmarks
News
- 2013-02:
Released
Download
SWW Benchmarks
Description
- This set
of benchmark examples was used in the experiments of software workaround
of microprocessor errors of the following paper.
References
Tsung-Po Liu,
Shuo-Ren Lin, and Jie-Hong R. Jiang. Software Workarounds for Hardware
Errors: Instruction Patch Synthesis. IEEE Transactions on
Computer-Aided Design of Integrated Circuits and Systems (TCAD), to
appear.
|
| |
SLOG: Solving String Constraints with Logic Circuits
Authors
- Hung-En Wang, Tzung-Lin Tsai, Chun-Han Lin, Fang Yu, Jie-Hong R. Jiang
Contacts
- b99901038@ntu.edu.tw (HEW), jhjiang@ntu.edu.tw (JHJ)
Download
SLOG, linux 64 bit binary
Description
- SLOG is an automata-based string constraint solver, which is built on top of the UC Berkeley logic synthesis and verification system ABC. SLOG uses logic circuits to represent nondeterministic finite automata (NFA), and supports various string operations (e.g., intersection, union, concatenation, deletion, replacement, etc.) with counterexample generation capability [1]. For tool usage, please refer to the readme file.
Usages
- For command usage, see the readme file.
Benchmark
benchmark.tar.gz
- A small fraction of the benchmark used in experiment of [1].
To run SLOG with an instance, run the following command under the "[instance_number]/_blif" directory.
[path-to-binary]/abc <command.cmd
Where "command.cmd" is a file that indicate a series of automata operations in the instance.
References
[1] Hung-En Wang, Tzung-Lin Tsai, Chun-Han Lin, Fang Yu, Jie-Hong R. Jiang:
String Analysis via Automata Manipulation with Logic Circuit Representation.
In Proceedings of the International Conference on Computer Aided Verification (CAV), 2016.
|
| |
QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving
Authors
- Kuan-Hua Tu, Tzu-Chen Hsu, Jie-Hong R. Jiang
Contacts
- isuis3322@gmail.com (KHT); jhjiang@ntu.edu.tw (JHJ)
Download
QELL, linux 64 bit binaries
Description
- QELL is a QBF solver using levelized SAT solving in the flavor of formula expansion. Learning techniques based on circuit structure reconstruction, complete and incomplete ALLSAT learning, clauses selection, core expansion, bounded recursion, and other methods are devised to control formula growth.
To Use:
- ./QELL [-cpu-lim=<int>] <filename>
References
[1] QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving
Kuan-Hua Tu, Tzu-Chen Hsu, and Jie-Hong R. Jiang
The 18th International Conference on Theory and Applications of Satisfiability Testing (SAT 2015)
|
