Testing, Verification, and Analysis of Software

String Variables and String Constraints

Constraints on strings of unknown length occur in a wide variety of real-world problems in software/hardware testing, verification, and analysis: examples are test case generation, program analysis, model checking, and web security.

We proposed [SFP13, SFP15] the addition of bounded-length string decision variables and string constraints (such as CONCAT, REVERSE, SUBSTRING, etc) to constraint-based modelling languages and CP solvers, reminding also of a simple default way [HFP13b] of implementing them via fixed-length arrays. Experiments show that CP solvers belong to the state of the art for constraint solving over fixed-length and bounded-length string variables.

Also see Pierre Flener's invited lecture on string variables in verification at the Master Class on CP and Verification at CPAIOR 2015.

Test-Case Generation

Selected publications: [BGP14, CGP14]

Events

CP meets Verification: 2012, 2014

Workshops on Constraints in Software Testing, Verification, and Analysis: CSTVA 2006, CSTVA 2010, CSTVA 2011, CSTVA 2012, CSTVA 2013, CSTVA 2014