Bibliographic record
Abstract
Les analyses interprocédurales automatiques de programmes qui sont basées sur des théories mathématiques rigoureuses sont complexes à réaliser, mais elles sont d'excellents outils pour augmenter notre conance envers les comportements possibles d'un programme. Les méthodes classiques pour réaliser ces analyses sont l'analyse de modè- les, l'interprétation abstraite et la démonstration automatique de théorèmes. La base d'un démonstrateur automatique de théorèmes est une logique ou une algèbre et le choix de celle-ci a un impact sur la complexité de trouver une preuve pour un théorème donné. Cette dissertation développe un formalisme algébrique concis pouvant être utilisé en démonstration automatique de théorèmes. Ce formalisme est appellé algèbre de Kleene à pile visible. Cette dissertation explique comment ce formalisme peut être utilisé pour réaliser des analyses interprocédurales de programmes, comme des vérications formelles et des vérications d'optimisations efectuées par des compilateurs. Cette dissertation apporte aussi des preuves que ces analyses pourraient être automatisées. L'algèbre de Kleene à pile visible est une extension de l'algèbre de Kleene, un excellent formalisme pour réaliser des analyses intraprocédurales de programmes. En bref, l'algèbre de Kleene est la théorie algébrique des automates nis et des expressions régulières. Donc, cette algèbre à elle seule n'est pas appropriée pour faire des analyses interprocédurales de programmes car la puissance des langages non contextuels est souvent nécessaire pour représenter le lot de contrôle d'un tel programme. L'algèbre de Kleene à pile visible étend celle-ci en lui ajoutant une famille d'opérateurs de plus petit point xe qui est basée sur une restriction des grammaires non contextuelles. En fait, cette algèbre axiomatise exactement la théorie équationnelle des langages à pile visibles. Ces langages sont une sous-classe des langages non contextuels et ont été dénis par Alur et Madhusudan pour faire de l'analyse de modèles. La complexité résultante de la théorie équationnelle de l'algèbre proposée est EXPTIME-complète.
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.
How this classification was reachedexpand
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.000 | 0.000 |
| Meta-epidemiology (narrow) | 0.000 | 0.001 |
| Meta-epidemiology (broad) | 0.001 | 0.001 |
| Bibliometrics | 0.001 | 0.004 |
| Science and technology studies | 0.001 | 0.000 |
| Scholarly communication | 0.000 | 0.001 |
| 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 itClassification
machine, unvalidatedMachine predicted; a candidate call from one teacher head, not a consensus.
How this classification was reached, model by model and score by score, is at the end of the page under "How this classification was reached".