X-by-Construction: Towards Ensuring Non-Functional Properties in by-Construction(…)
summary
Proposes generalizing X-by-Construction to non-functional properties, defines six concrete requirements for a property to fit into by-construction workflows, and prototypes energy annotations using four uninterpreted symbols for read/write/binary/return operations. Applies refinement-based construction to linear search, incrementally resolves undefined energy annotations, and maps them to a PTX instruction-level energy model to show a crossover (about 12 elements) where binary search becomes more energy-efficient. Notes gaps to hardware models, compositionality limits, and missing tool support.
AI-written summary · about
chapters (12)
- 0:00Introduction to X-by-Construction
- 1:27Software quality beyond correctness
- 3:13Correctness by Construction
- 7:06Challenges of post-hoc verification
- 8:55Vision for X-by-Construction
- 13:36Requirements for non-functional properties
- 15:02Focusing on energy efficiency
- 17:34Energy annotations in CBC refinement
- 20:24Comparing algorithm families by energy
- 21:51Limitations and future challenges
- 23:19Current work and next steps
- 24:44Q&A
related talks
15mCorrectness-by-Construction for Feature-Oriented Software Product Lines
23mFormal Methods to Save the Earth
31mCooperative Specification via Composition Control
01h 05m“Contract Programming in C++(20) (part 2 of 2)”
19mSynthesizing Specifications
52mThink Abstractly, Work Concretely
20mA Modular Approach to Metatheoretic Reasoning for Extensible Languages
01h 18mProper Inheritance