National Repository of Grey Literature 1 records found  Search took 0.01 seconds. 
Length Constraints in String Solving
Hranička, Jan ; Lengál, Ondřej (referee) ; Havlena, Vojtěch (advisor)
Řešení řetězcových omezení je v dnešní době základním kamenem formální verifikace s širokým vědeckým i obchodním uplatněním. Přínosem této práce je návrh nové rozhodovací procedury s cílem rozšířit jeden z předních string solverů: Z3-Noodler. Tato rozhodovací procedura je založena na symbolickém zarovnání řetězcových proměnných v rovnicích pomocí generování omezení na jejich délky. Experimenty na standartních benchmarcích ukázaly, že integrace této procedury s nástrojem Z3-Noodler vede ke snížení timeoutů o 32 a na určitých testech snižuje celkovou dobu běhu nástroje více než padesátkrát. Díky těmto přínosům je možné očekávat přidání této procedury do zmíněného nástroje.

Interested in being notified about new results for this query?
Subscribe to the RSS feed.