Skip to main content

23 posts tagged with "goedel"

View All Tags

· One min read
James Chapman

The team works on applied research and consulting in formal methods that is directly applicable to evidence based engineering in Core Tech and beyond.

High level summary​

The team is currently formalising mini protocols and testing the performance analysis tool

Details​

  • drafting processs calculus semantics of mini protocol programs

  • testing the new performance modelling tool

  • further work on specification of mini protocols

  • extension of mini protocol framework to support communication of programs with local environments via synchronous channels

· One min read
James Chapman

The team works on applied research and consulting in formal methods that is directly applicable to evidence based engineering in Core Tech and beyond.

High level summary​

The team is currently formalising mini protocols and also further developing the performance modelling prototype.

Details​

  • working on collating and open sourcing performance analysis prototype

  • improvements to Ouroboros Praos specification in Isabelle

  • working on formalising chain sync mini-protocol

  • reviewing an alternatice semantics for DeltaQ

  • Seminar talk at U. Bergen on algebraic properties of timeliness

· One min read
James Chapman

The team works on applied research and consulting in formal methods that is directly applicable to evidence based engineering in Core Tech and beyond.

High level summary​

The team is currently formalising mini protocols and also further developing the performance modelling prototype.

Details​

  • finalising a presenting performance analysis internship work to the formal methods team

  • developed a new Isabelle mini-protocol framework and examples

  • planning an extended version of the ICE DeltaQ paper

  • working on algebraic rules for properisation of any-to-finish

· One min read
James Chapman

The team works on applied research and consulting in formal methods that is directly applicable to evidence based engineering in Core Tech and beyond.

High level summary​

The team is currently formalising mini protocols and also further developing the performance modelling prototype.

Details​

  • Development of an automated prover for showing conformance of programs to state machines (as part of the mini-protocol framework)

  • Completion of the documentation of the (current state of the) mini-protocol framework

  • Discussion about two DeltaQ lectures with two practical sessions as part of 4th year masters course on distributed systemsby colleagues at UC Louvain in the Autumn

  • Discussion about four DeltaQ lectures by colleagues at U. Bergen as part of a 5th year Masters course in the Autumn

  • Adapted original DeltaQ implementation to the new typeclasses and wrote property tests for its algebraic laws

· One min read
James Chapman

The team works on applied research and consulting in formal methods that is directly applicable to evidence based engineering in Core Tech and beyond.

High level summary​

The team is formalising mini protocols and also further developing the performance modelling prototype.

Details​

  • Developing new framework for specification and verification of mini-protocols which is closer to the Haskell implementation.

  • Developed a new internal representation for the DeltaQ algebra that allows for more modularity in backend implementations

  • Discussions regarding the Cardano networking specification