Zobrazeno 1 - 10
of 313
pro vyhledávání: '"Jones, Cliff"'
Hoare-style inference rules for program constructs permit the copying of expressions and tests from program text into logical contexts. It is known that this requires care even for sequential programs but further issues arise for concurrent programs
Externí odkaz:
http://arxiv.org/abs/2409.07741
Specifications of significant systems can be made short and perspicuous by using abstract data types; data reification can provide a clear, stepwise, development history of programs that use more efficient concrete representations. Data reification (
Externí odkaz:
http://arxiv.org/abs/2405.05546
Autor:
Jones, Cliff B., Burns, Alan
The reference point for developing any artefact is its specification; to develop software formally, a formal specification is required. For sequential programs, pre and post conditions (together with abstract objects) suffice; rely and guarantee cond
Externí odkaz:
http://arxiv.org/abs/2312.00171
The verification of security protocols is essential, in order to ensure the absence of potential attacks. However, verification results are only valid with respect to the assumptions under which the verification was performed. These assumptions are o
Externí odkaz:
http://arxiv.org/abs/2311.15189
Autor:
Jones, Cliff B, Burns, Alan
Publikováno v:
Mathematical Foundations of Software Engineering, College Publication, 2022, Chap 6
The application considered is mixed-criticality scheduling. The core formal approaches used are Rely-Guarantee conditions and the Timeband framework; these are applied to give a layered description of job scheduling which includes resilience to jobs
Externí odkaz:
http://arxiv.org/abs/2012.01493