
ResQu
News
 201107: Version 0.1 released
 201305: Version 1.0 released (now also works with QRP)
 201405: Version 2.0 released (can perform certificate minimization)
 201501: Version LP released (works with LQ resolution proofs)
Description
 ResQu is a tool for deriving Herbrand/Skolem functions from Qresolution and Qconsensus proofs.
 Input formats:
 QBC (proof formats of Squolem, EBDDRES);
 Proof format of Qubecert;
 QRP (Proof format of cDepQBF);
 RFAO (local input format as a rightfiratandor formula just for certificate optimization)
 Output formats: BLIF (format of ABC synthesis tool), RFAO (same as above)
Link
ResQu


Software Workaround Benchmarks
News
 201302:
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
TsungPo Liu,
ShuoRen Lin, and JieHong R. Jiang. Software Workarounds for Hardware
Errors: Instruction Patch Synthesis. IEEE Transactions on
ComputerAided Design of Integrated Circuits and Systems (TCAD), to
appear.




SLOG: Solving String Constraints with Logic Circuits
Authors
 HungEn Wang, TzungLin Tsai, ChunHan Lin, Fang Yu, JieHong R. Jiang
Contacts
 b99901038@ntu.edu.tw (HEW), jhjiang@ntu.edu.tw (JHJ)
Download
SLOG, linux 64 bit binary
Description
 SLOG is an automatabased 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.
[pathtobinary]/abc <command.cmd
Where "command.cmd" is a file that indicate a series of automata operations in the instance.
References
[1] HungEn Wang, TzungLin Tsai, ChunHan Lin, Fang Yu, JieHong 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
 KuanHua Tu, TzuChen Hsu, JieHong 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 [cpulim=<int>] <filename>
References
[1] QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving
KuanHua Tu, TzuChen Hsu, and JieHong R. Jiang
The 18th International Conference on Theory and Applications of Satisfiability Testing (SAT 2015)


Homing Sequence QBF Benchmarks
Authors
 HungEn Wang, KuanHua Tu, JieHong R. Jiang
Contacts
 isuis3322@gmail.com (KHT); jhjiang@ntu.edu.tw (JHJ)
Download
nonadaptivehoming.tar.gz
Description
 The zip file contains the QBF benchamrks of the following ICTSS paper for checking the existence of nonadaptive homing sequence of nondeterministic finite state machines (NFSMs). For each of the 25 FSMs, 4 to 5 length constaints are created. There are 101 qdimacs files in total. The qdimacs file name indicates the original FSM case and length constaint information. For example, "15_states_8_inputs_3_1.qdimacs" is checking the existence of homing sequence of the 3rd FSM from the 15_states_8_inputs group with length constaint 1. The QBF is false iff a homing sequence exists.
Reference
HungEn Wang, KuanHua Tu, JieHong R. Jiang, and Natalia Kushik.
Homing Sequence Derivation with Quantified Boolean Satisfiability.
In Proc. IFIP International Conference on Testing Software and Systems (ICTSS), pp. 230242, 2017.



