Abstract-This paper presents the ELdarica version 2 model checker. Under de senaste åren har vi utvecklat och underhållit ELDARICA som en toppmodern lösare för Horn klausuler över heltal aritmetik. I version 2 har vi utökat lösaren till att stödja även algebraiska datatyper och bit-vektorer, teorier som ofta tillämpas i verifiering, men som för närvarande inte stöds av de flesta Horn lösare. I detta dokument beskrivs verktygets struktur på hög nivå och det gränssnitt som det tillhandahåller till andra tillämpningar. Vi rapporterar också om en utvärdering av verktyget. Även om några av teknikerna i ELDARICA har dokumenterats i forskningsrapporter under de senaste åren, är detta det första verktygspapper som beskriver ELDARICA i sin helhet.
Enligt vår kunskap är Eldarica REF den enda CHC-lösaren som stöder algebraiska datatyper.
The ELDARICA Horn Solver
{'venue': '2018 Formal Methods in Computer Aided Design (FMCAD)', 'journal': '2018 Formal Methods in Computer Aided Design (FMCAD)', 'mag_field_of_study': ['Computer Science']}