unknown
 
| About ALCom | News | People | Research | Publications | Tools | Student Info | Links |
unknown

 

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)

 


 

Homing Sequence QBF Benchmarks

Authors

      -  Hung-En Wang, Kuan-Hua Tu, Jie-Hong R. Jiang 

Contacts

      -  isuis3322@gmail.com (KHT); jhjiang@ntu.edu.tw (JHJ) 

Download

      non-adaptive-homing.tar.gz

Description

      - The zip file contains the QBF benchamrks of the following ICTSS paper for checking the existence of non-adaptive 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

     Hung-En Wang, Kuan-Hua Tu, Jie-Hong R. Jiang, and Natalia Kushik. Homing Sequence Derivation with Quantified Boolean Satisfiability. In Proc. IFIP International Conference on Testing Software and Systems (ICTSS), pp. 230-242, 2017.

   
© 2007 Applied Logic and Computation Laboratory, GIEE, NTU. All rights reserved.