Name
Abstract | ||
|---|---|---|
A popular technique in regular expression matching accelerators is to decompose a regular expression and communicate through instructions executed by a post-processor. We present a complete verification method that leverages the success of sequential equivalence checking (SEC) to proving correctness of the technique. The original regular expression and the system of decomposed regular expressions are modeled as net-lists and their equivalence is proved using SEC. SEC proves correct handling of 840 complex patterns from the Emerging Threats open rule set in 50 hours, eliminating altogether informal simulation and testing. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1145/2228360.2228424 | DAC |
Keywords | Field | DocType |
sequential equivalence checking,regular expression,proving correctness,popular technique,correct handling,emerging threats,informal simulation,regular expression accelerator,complete verification method,complex pattern,original regular expression,decomposed regular expression,hardware,formal verification,optimization,theorem proving,registers,equivalence checking,sec,engines,impedance matching,testing | Erbium doped fiber amplifier,Formal equivalence checking,Regular expression,Programming language,Computer science,Correctness,Automated theorem proving,Theoretical computer science,Equivalence (measure theory),Formal verification | Conference |
ISSN | Citations | PageRank |
0738-100X | 2 | 0.37 |
References | Authors | |
9 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mitra Purandare | 1 | 81 | 5.49 |
| Kubilay Atasu | 2 | 416 | 26.73 |
| Christoph Hagleitner | 3 | 108 | 20.84 |