You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: Docs/docs/whatisP.md
-2Lines changed: 0 additions & 2 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -58,8 +58,6 @@ Although the current P checker is great at finding _deep-hard-to-find_ bugs ("[H
58
58
We are actively working on addressing this challenge and are building two new backends for P. First, a _symbolic execution engine_ that can scale the P checker to models of large
59
59
distributed systems and provide **sound guarantees** of exploring all possible behaviors. Second, a deductive verification engine to perform **mathematical proof** of correctness for P programs. Both these backends will be released publicly soon.
60
60
61
-
[^1]: They are currently maintained in the dev branch `symbolic-codegen`.
62
-
63
61
#### Code Generation
64
62
65
63
The P compiler currently generates C# and C code. The generated code when combined with the P Runtime (that executes the P state machines) can be deployed on any target platform.
0 commit comments