{"schema_version":1,"experiment_id":"eoa_inverse_innovation_exp04_retrieval_first_paired20_20260802","cell_id":"computability_boundary_mapping__engineering_design","round_index":0,"assessments":[{"hypothesis_id":"H1","search_queries":["program equivalence undecidable arbitrary programs firmware equivalence checking official paper","translation validation embedded software equivalence checking firmware paper","product equivalence and context-free grammars decidable class IBM Research"],"sources":[{"source_id":"H1-S1","title":"Well structured program equivalence is highly undecidable","publisher":"arXiv / Goldblatt and Jackson","url":"https://arxiv.org/abs/1103.1433","source_class":"PRIMARY_RESEARCH","claims_supported":["Program-equivalence constructions can induce very strong undecidability results even for well-structured programs.","The exact result depends on the program logic and equivalence semantics, so it does not itself establish undecidability for every firmware model."]},{"source_id":"H1-S2","title":"Program equivalence and context-free grammars","publisher":"IBM Research","url":"https://research.ibm.com/publications/program-equivalence-and-context-free-grammars","source_class":"PRIMARY_RESEARCH","claims_supported":["Strong equivalence is undecidable for arbitrary systems of recursion equations.","A nontrivial restricted class associated with LL(k) grammars has decidable equivalence, illustrating the established pattern of replacing unrestricted equivalence with a decidable subclass."]},{"source_id":"H1-S3","title":"Translation Validation for a Verified OS Kernel","publisher":"University of Cambridge / PLDI","url":"https://www.cl.cam.ac.uk/~mom22/pldi13.pdf","source_class":"PRIMARY_RESEARCH","claims_supported":["The seL4 work proves refinement between C-source and binary semantics for a specific restricted verification setting.","It uses a shared restricted intermediate language and explicit omissions, demonstrating model-specific firmware or systems-software equivalence evidence rather than a universal checker."]}],"closest_analogue":"Model-specific translation validation for seL4 combined with established undecidability boundaries and decidable subclasses for program equivalence.","overlap":"The analogue already rejects unrestricted equivalence in favor of precisely defined semantics, restricted representations, and per-program proof obligations; it also shows that equivalence conclusions depend on the declared program class.","remaining_difference":"The located sources do not describe a certification-gate procedure that requires an independently checked, answer-preserving halting reduction before approving an unrestricted firmware-equivalence requirement. The testable distinction is whether this mandatory authorization-stage reduction review exists in firmware certification practice and measurably changes funding or scope decisions.","classification":"POSSIBLE_DISTINCTION","disposition":"ADVANCE","rationale":"The mathematical boundary and restricted verification response are established, but the proposed intervention may differ as a governance mechanism applied before project authorization. Advancement is only for testing that workflow-level distinction, not for claiming novelty in program-equivalence undecidability."},{"hypothesis_id":"H2","search_queries":["sound abstraction model checking controller safety hybrid systems primary research","SpaceEx reachability analysis hybrid systems official documentation abstraction","sound over approximation controller safety abstraction spurious counterexamples"],"sources":[{"source_id":"H2-S1","title":"Robust Abstractions for Control Synthesis: Completeness via Robustness for Linear-Time Properties","publisher":"ACM HSCC","url":"https://doi.org/10.1145/3049797.3049826","source_class":"PRIMARY_RESEARCH","claims_supported":["The paper constructs sound abstractions for uncertain transition systems and nonlinear control systems.","The abstractions preserve robust satisfaction of linear-time properties and support provably correct controller synthesis."]},{"source_id":"H2-S2","title":"SpaceEx with CEGAR","publisher":"RWTH Aachen University, Theory of Hybrid Systems","url":"https://ths.rwth-aachen.de/research/tools/spaceex-with-cegar/","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","claims_supported":["SpaceEx with CEGAR performs reachability analysis of hybrid systems using counterexample-guided abstraction refinement.","The first-party project distributes the tool, documentation, and benchmarks."]},{"source_id":"H2-S3","title":"Discrete Abstractions of Hybrid Systems: Verification of Safety and Application to User-Interface Design","publisher":"NASA Technical Reports Server","url":"https://ntrs.nasa.gov/citations/20040000797","source_class":"GOVERNMENT_OR_REGULATOR","claims_supported":["The method computes invariant safe regions for hybrid control systems and derives discrete abstractions from them.","It demonstrates the method on automotive and aircraft-autopilot examples and claims mathematical safety guarantees under the modeled controller and boundary conditions."]}],"closest_analogue":"Sound finite abstraction and reachability/model checking of hybrid controllers, including SpaceEx-style CEGAR and NASA hybrid-safety abstractions.","overlap":"Finite abstraction of controller–plant behavior, sound safety reasoning, reachability analysis, refinement of potentially spurious counterexamples, and application to physical control systems are all directly represented.","remaining_difference":"The seeded-hazard benchmark and alarm-burden study are evaluation details rather than a distinct technical mechanism; they could test an implementation but do not separate the hypothesis from the established abstraction-based verification approach.","classification":"OBVIOUS_COLLISION","disposition":"REJECT","rationale":"The proposed causal lever is the standard sound-abstraction/model-checking pattern already developed and applied to hybrid control safety. The proposed validation protocol does not create a material remaining distinction."},{"hypothesis_id":"H3","search_queries":["enumerative program synthesis timeout unknown infeasible official tool documentation","SyGuS solver unknown timeout status standard","enumerative synthesis fail versus infeasible unrealizability proof"],"sources":[{"source_id":"H3-S1","title":"The SyGuS Language Standard Version 2.0","publisher":"SyGuS","url":"https://sygus-org.github.io/assets/pdf/SyGuS-IF_2.0.pdf","source_class":"STANDARD","claims_supported":["The standard distinguishes a returned synthesized definition, `infeasible` meaning no solution, and `fail` meaning the solver failed to find a solution.","A returned definition is only correct when it satisfies the stated syntactic and semantic restrictions."]},{"source_id":"H3-S2","title":"Synthesizing Imperative Programs from Examples Guided by Static Analysis","publisher":"arXiv / SIMPL authors","url":"https://arxiv.org/abs/1702.06334","source_class":"PRIMARY_RESEARCH","claims_supported":["SIMPL enumerates candidate programs in increasing size and uses sound static-analysis pruning.","The paper separates finding a candidate from validating it against the supplied examples and constraints."]},{"source_id":"H3-S3","title":"Proving Unrealizability for Syntax-Guided Synthesis","publisher":"arXiv / NOPE authors","url":"https://arxiv.org/abs/1905.05800","source_class":"PRIMARY_RESEARCH","claims_supported":["A separate proof method is needed to establish unrealizability for synthesis problems.","Existing SyGuS solvers timed out on benchmarks for which the proposed method could sometimes prove unrealizability, directly showing that timeout is not an infeasibility proof."]}],"closest_analogue":"The SyGuS output protocol’s explicit separation of a valid solution, `infeasible`, and solver `fail`, supplemented by certificate-producing unrealizability analysis.","overlap":"Enumerative candidate search, witness-bearing success, bounded or failed search that is not treated as infeasibility, and separate proof obligations for genuine unrealizability all coincide with the hypothesis.","remaining_difference":"Renaming `fail` as `UNKNOWN` and applying the same output discipline to engineering concepts does not supply a distinct mechanism. Dovetailing multiple generators is an implementation choice within the already-established fail-versus-infeasible protocol.","classification":"OBVIOUS_COLLISION","disposition":"REJECT","rationale":"A directly applicable synthesis standard already encodes the central intervention: failure to find a solution is distinct from proof that none exists."},{"hypothesis_id":"H4","search_queries":["CAD product configuration rule language termination decidable fragment recursion official","product configuration language decidable description logic configuration engineering research","CAD design rule language termination recursion product configurator official documentation"],"sources":[{"source_id":"H4-S1","title":"A Dynamic Logic for Configuration","publisher":"CEUR Workshop Proceedings / Max Planck Institute for Informatics","url":"https://ceur-ws.org/Vol-1770/ARQNL2016_paper3.pdf","source_class":"PRIMARY_RESEARCH","claims_supported":["PIDL+ is motivated by real configuration systems for steel and power plants, including Siemens practice.","It uses finitely bounded transition variables and syntactic admissibility conditions to preserve decidability.","It provides sound and complete algorithms, finite transition graphs, rule-terminal states, and decidable soundness and completeness checks."]},{"source_id":"H4-S2","title":"An Evaluation of Description Logic for the Development of Product Models","publisher":"National Institute of Standards and Technology / GovInfo","url":"https://www.govinfo.gov/content/pkg/GOVPUB-C13-db59e7c73ad9ca80bcaae25b560991fd/pdf/GOVPUB-C13-db59e7c73ad9ca80bcaae25b560991fd.pdf","source_class":"GOVERNMENT_OR_REGULATOR","claims_supported":["The report evaluates OWL-DL expressivity and SWRL rules for product assembly models in a manufacturing context.","It demonstrates an established engineering-design use of restricted logical languages and reasoners for product rules."]}],"closest_analogue":"PIDL+, a decidable rule language explicitly designed for interactive industrial product configuration in steel and power-plant settings.","overlap":"An enforceable restricted language, bounded rule-relevant variables, terminating rule-to-fixpoint behavior, decidable configuration properties, and explicit expressiveness restrictions are already present in the closest analogue.","remaining_difference":"Version-linked reclassification triggers are an added governance record, but they do not materially distinguish the proposed decidable-fragment mechanism from PIDL+. They could be appended routinely to an existing language-release process.","classification":"OBVIOUS_COLLISION","disposition":"REJECT","rationale":"The closest source is not merely adjacent theory; it is a decidable configuration language motivated by the same industrial workflow and built around the same expressiveness-for-termination trade."},{"hypothesis_id":"H5","search_queries":["multidisciplinary design optimization simulation failure hidden failure handling external analysis code","OpenMDAO analysis error failure optimization documentation AnalysisError","DAKOTA simulation failure handling interface failure capture optimization official manual"],"sources":[{"source_id":"H5-S1","title":"Raising an AnalysisError","publisher":"OpenMDAO Development Team","url":"https://openmdao.org/newdocs/versions/latest/advanced_user_guide/analysis_errors/analysis_error.html","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","claims_supported":["OpenMDAO components can explicitly raise an AnalysisError for invalid analysis regions.","Optimizer responses vary; the documentation warns that some optimizers may fail or even find an incorrect solution after analysis errors."]},{"source_id":"H5-S2","title":"analysis_error.py","publisher":"OpenMDAO Development Team","url":"https://openmdao.org/newdocs/versions/latest/_srcdocs/packages/core/analysis_error.html","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","claims_supported":["OpenMDAO defines AnalysisError as a distinct exception for a possibly recoverable numerical error in an analysis code or subsolver."]},{"source_id":"H5-S3","title":"Simulation Failure Capturing","publisher":"Sandia National Laboratories, Dakota","url":"https://snl-dakota.github.io/docs/6.19.0/users/usingdakota/advanced/simulationfailurecapturing.html","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","claims_supported":["Dakota explicitly separates failure detection, communication, and mitigation for external simulations.","Supported reactions include abort, retry, recovery with declared dummy values, and continuation; the user remains responsible for domain-specific detection.","The documentation recognizes transient external causes such as licensing, networking, and shared storage."]},{"source_id":"H5-S4","title":"Dakota interface reference","publisher":"Sandia National Laboratories, Dakota","url":"https://snl-dakota.github.io/docs/6.18.0/users/usingdakota/reference/interface.html","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","claims_supported":["Dakota defines its interface as the bridge between optimization variables and underlying simulation codes.","The interface exposes an explicit failure-capture option controlling responses to analysis-driver failure."]}],"closest_analogue":"Dakota’s external-simulation failure-capture interface, with OpenMDAO’s explicit AnalysisError propagation and optimizer-dependent recovery behavior.","overlap":"External analysis calls are modeled as fallible; failures have explicit detection and communication paths; routing can abort, retry, recover, or continue; and documentation warns against assuming every optimizer preserves correctness after an error.","remaining_difference":"The sources focus on computational simulations and numerical subsolvers, not vendor refusal, laboratory unavailability, inconsistent expert judgment, mechanically checked input promises, or a rule forbidding every unqualified feasibility/optimality verdict after those non-computational failures. A testable distinction is whether an MDO framework implements a typed contract spanning simulator, laboratory, vendor, and human-evaluator failures while preserving a labeled unresolved state at the design gate.","classification":"POSSIBLE_DISTINCTION","disposition":"ADVANCE","rationale":"Existing tools collide with much of the failure-routing mechanism, but the broader oracle contract across human, laboratory, and vendor capabilities—and its preservation of unresolved status through the final design verdict—was not found in this shallow screen."}],"nominated_ids":["H1","H5"],"replenishment_recommended":false}