Verifying finite-state properties of large-scale programs
Why this work is in the frame
A frame that forgets how it found something cannot be audited. These are the routes that admitted this work.
Bibliographic record
Abstract
Les concepteurs des différentes composantes logicielles peuvent utiliser les propriétés des automates finis pour fixer les spécifications de l'interface comportementale qui contrôleront les règles de programmations définissant l'utilisation des composantes. Ceci permet aux utilisateurs de ces composantes de vérifier le respect de ses règles par leurs codes sources, à la fois lors d'une analyse statique qu'à l'exécution. Dans cette dissertation, nous montrerons la conception de Clara, une structure qui permet de spécifier et de vérifier les propriétés des automates finis dans des programmes étendus, puis expliquerons son implantation. Le programmeur, à l'aide de Clara, peut définir les propriétés des automates finis en complément aux processus de vérification à l'exécution, en utilisant une extension de la syntaxe d'AspectJ, un langage de programmation orienté aspect. Clara utilise alors, en séquence, trois analyses statiques de précision croissante pour déterminer si le programme respecte les propriétés des automates finis. Clara produit une liste des positions dans le code source où il y a risque de violation de ces «propriétés», en ordre décroissant de certitude d'une violation. Quand cela est possible, Clara ajoute au programme des processus de vérification permettant d'étudier la violation de «propriétés» lors de son exécution. Grâce à son analyse statique, Clara n'ajoute pas au code ces processus dans les portions de code qui n'ont pas la possibilité de violer les propriétés des automates finis, ce qui limite les ralentissements dus aux processus de vérification. Lorsque ses ajouts restent considérables, Clara organise les processus de vérification à l'exécution en sous-groupe, de sorte qu'il soit possible de distribuer différentes versions du programme contenant seulement une partie de ceux-ci, limitant ainsi l'utilisation des ressources système à l'exécution. Nous avons validé cette approche en soumettant à Clara les propriétés des automates finis sous différents modèles à appliquer sur différents programmes Java. Clara a permis de prouver que la plupart de ces programmes respectaient déjà les propriétés définies. Dans les autres cas, Clara a pu réduire le coût des processus de vérification à moins de 10%. De plus, nous avons pu localiser de nombreuses violations de propriété manuellement, en inspectant les entrées en importance dans la liste produite par Clara.
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
Full frame distilled prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. Learned from the 10,348 direct Codex labels and 10,348 direct Gemma labels. Candidate is the union of thresholded teacher heads; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels or direct frontier model labels.
Codex and Gemma teacher scores by category
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.002 | 0.003 |
| Meta-epidemiology (narrow) | 0.000 | 0.000 |
| Meta-epidemiology (broad) | 0.001 | 0.000 |
| Bibliometrics | 0.000 | 0.001 |
| Science and technology studies | 0.000 | 0.000 |
| Scholarly communication | 0.000 | 0.002 |
| Open science | 0.002 | 0.001 |
| Research integrity | 0.000 | 0.001 |
| Insufficient payload (model declined to judge) | 0.000 | 0.000 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from it