PhD Opportunities in Computer Science (Fully Funded)
R@ISE Project (University of Limerick)
See the full job description on jobRxiv: https://jobrxiv.org/job/rise-project-university-of-limerick-27778-phd-opportunities-in-computer-science-fully-funded/?feed_id=91424
#computer_science #formal_methods #model_driven_development #software_engineering #ScienceJobs #...
https://jobrxiv.org/job/rise-project-university-of-limerick-27778-phd-opportunities-in-computer-science-fully-funded/?feed_id=91424
Verified Effectful Programming in F* - Catalin Hritcu
- yewtu.be [https://yewtu.be/watch?v=SPCko8ACB0M] - inv.nadeko.net [https://inv.nadeko.net/watch?v=SPCko8ACB0M] - yt.artemislena.eu [https://yt.artemislena.eu/watch?v=SPCko8ACB0M] - piped.video [https://piped.video/watch?v=SPCko8ACB0M] I noticed that not many people in the formal methods world have even heard of F Star. From what I’m told by people much more advanced than myself, it goes even further than Agda and Coq in proving correctness. I’d like to understand why if someone would explain.
PhD Opportunities in Computer Science (Fully Funded)
R@ISE Project (University of Limerick)
See the full job description on jobRxiv: https://jobrxiv.org/job/rise-project-university-of-limerick-27778-phd-opportunities-in-computer-science-fully-funded/?feed_id=91060
#computer_science #formal_methods #model_driven_development #software_engineering #ScienceJobs #...
https://jobrxiv.org/job/rise-project-university-of-limerick-27778-phd-opportunities-in-computer-science-fully-funded/?feed_id=91060
A couple years back I was introduced to some of the folks at Galois, and they convinced me that formal methods can lower the cost of software development. Now I’m reading this post from @marcbrooker where he adds a bit of nuance that I think is helpful. I’ll summarize it this way: formal methods can lower the total cost to develop and maintain system-level software, where the requirements are stable and well-understood. If you’re designing a user-facing system and need to interatively respond to customer feedback—in other words, if your requirements are shifting and poorly understood—Agile remains the best choice.
We have released version 1.6.2 of CafeOBJ, an algebraic specification and verification language. It has been a long time since we made a formal release. There has been an internal release that really never got published, and just to rectify this, plus a few changes, a new release was made.…
There's now a video up of the talk I gave at this year's seL4 Summit, on the status of UNSW's projects to verify Time Protection and Microkit-based userland OS services for the seL4 microkernel:
#sel4summit #seL4 #verification #operatingsystems #microkernel #IsabelleHOL #HOL4 #ITP #modelchecking #formalmethods #formalverification #formal_methods #formal_verification
Like 4 people favourited my post about Nix.
This is the height of viral fame for me.
Social media isn't bad when there's zero marketing budget, no anger/attention/algorithm bullshit.
Anyway, I'm trying to package this with Nix:
https://github.com/SamueleGerminiani/harm
I'm working through a CMake issue - the C++ can't find antlr4-runtime.h. Follow along for the gory details as I succeed or fail miserably!
Okay, so first test of Yosys-Synlig for formal methods, it looks like everything was deemed non-synthesizable and removed...
...But of course it was non-synthesizable, I was trying to create some assertions for formal verification.
It is unclear if I don't understand the proper use of SVA, or if the Surelog "front end" isn't spitting out a UHDM representation for property syntax?
Interested in this at all? Ping me. Using Nix flake to setup the build tools. #yosys #nix #formal_methods #UHDM
just made a nix flake so I could have a dev shell for yosys and synlig. Hopefully will make a plugin for Yosys to expand its formal verification abilities.
Or fail miserably because I don't know what I'm doing, tune in next week for self doubt, chaos and lots of gnashing of teeth!
jobRxiv
cyph3rPunk
Daniel Moch
Norbert Preining
Louise Dennis
Rob Sison
havoc