Many properties of programs and computer systems represented as first-order logical theories can be formulated as Boolean combinations of atoms where all variables are existentially quantified. The infChecker tool focuses on the analysis of such properties for rewrite-based programming languages. Its operation is completely automatic, with no need for the user to intervene other than to provide the problem to be treated. infChecker has participated with excellent results in international competitions along with tools of similar purpose.
Examples of use are: security properties of concurrent systems, non-termination of rewrite systems, verification of cryptographic protocols, etc.
Program verification, safety analysis, provable security. Protocol crypto-analysis. Automated analysis, modeling, verification, synthesis, learning, debugging and optimization of complex systems and models