000342677 001__ 342677
000342677 005__ 20230827173359.0
000342677 0247_ $$2CORDIS$$aG:(EU-Grant)101076510$$d101076510
000342677 0247_ $$2CORDIS$$aG:(EU-Call)ERC-2022-STG$$dERC-2022-STG
000342677 0247_ $$2originalID$$acorda_____he::101076510
000342677 035__ $$aG:(EU-Grant)101076510
000342677 150__ $$aTesting Program Analyzers Ad Absurdum$$y2023-07-01 - 2028-06-30
000342677 372__ $$aERC-2022-STG$$s2023-07-01$$t2028-06-30
000342677 450__ $$aMirandaTesting$$wd$$y2023-07-01 - 2028-06-30
000342677 5101_ $$0I:(DE-588b)5098525-5$$2CORDIS$$aEuropean Union
000342677 680__ $$aProgram analyzers act as guards for ensuring reliability of modern-day
software. But who guards the guards themselves? Due to their high
complexity and sophisticated algorithms, analyzers are likely to
contain critical bugs, which we define as those leading to wrong
results, e.g., returning `correct' for incorrect software. Such bugs
may have detrimental consequences, especially in safety-critical
settings. It is, therefore, imperative to be able to detect them.

Verifying the absence of critical bugs in a program analyzer is
prohibitively expensive. Contrary to verification, automated test
generation can be used to effectively find such bugs. Existing testing
approaches, however, are still in their infancy for this application
domain.

To address this issue, MirandaTesting will develop the first
principled methodology for testing a wide range of program
analyzers. At its core, our methodology exposes more information about
why an analyzer computes a particular result; it then uses this
information to interrogate the analyzer aiming to force it into a
contradiction, thus revealing a critical bug. The project has the
following goals:

1. Design a general framework for testing program analyzers using the
  MirandaTesting methodology;

2. Develop interrogation strategies pertaining to eleven prevalent
  classes of program analyzers;

3. Demonstrate the effectiveness of concrete instantiations of the
  general framework and interrogation strategies for several popular
  program analyzers from each class;

4. Focus on disseminating our methodology and infrastructure.

If successful, MirandaTesting will enable systematic testing of entire
program-analyzer classes. As a result, analyzers will exhibit fewer
critical bugs, potentially preventing catastrophic outcomes in
safety-critical domains.
000342677 909CO $$ooai:juser.fz-juelich.de:1012036$$pauthority:GRANT$$pauthority
000342677 909CO $$ooai:juser.fz-juelich.de:1012036
000342677 980__ $$aG
000342677 980__ $$aCORDIS
000342677 980__ $$aAUTHORITY