Home   >   Demonstrators   >   INFCHECKER

infChecker

Demonstrator|vrain

Description
Verification of existential formulas in rewrite rule-based programs
Member
vrain
Address
Camino de Vera S/N
Province
Valencia

DEMONSTRATOR INFORMATION

DESCRIPTION

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.

POSSIBILITIES

Examples of use are: security properties of concurrent systems, non-termination of rewrite systems, verification of cryptographic protocols, etc.

TECHNOLOGICAL ENABLER

Artificial Intelligence and Computing
Data security and privacy technologies

Program verification, safety analysis, provable security. Protocol crypto-analysis. Automated analysis, modeling, verification, synthesis, learning, debugging and optimization of complex systems and models