| 28 Nov 2022 |
 everett.hildenbrandt | It looks like you're already using solc-to-k, and the Foundry integration should be able to state all the properties you've posted here. | 15:46:48 |
| everett.hildenbrandt | But allows you to work fully in-solidity. | 15:46:54 |
 Enzo Evers | True. I tried following the rewrites in evm.md and found that it halts around the place I describe in this issue: https://github.com/runtimeverification/evm-semantics/issues/1469 | 15:48:39 |
| Enzo Evers | I haven't used the foundry integration of kevm yet. But I will try it too. | 15:49:15 |
| everett.hildenbrandt | As a (quick and hacky) workaround, you can modify KEVM to skip accessStorage step. | 15:57:42 |
| everett.hildenbrandt | But that is obviously not desirable long-term. | 15:57:49 |
| everett.hildenbrandt | You can do this like this:
rule k #accessStorage => . ... /k [priority(45)] | 15:58:09 |
| everett.hildenbrandt | Note this is not in general sound. | 15:58:28 |
| everett.hildenbrandt | But it will get you past this (rather silly) problem, so you can focus on more interesting things. | 15:58:43 |
| 16 Dec 2022 |
|  David changed their display name from David to David - OOO Fri Dec 16th. | 07:24:35 |
| 19 Dec 2022 |
|  franklinchen changed their profile picture. | 00:54:10 |
| David changed their display name from David - OOO Fri Dec 16th to David. | 07:03:29 |
| 23 Dec 2022 |
|  8ardamu joined the room. | 09:29:08 |
| 11 Jan 2023 |
| Enzo Evers | I have a question about how K parses to potential uses of reachability symbols. In reachability-symbols.md I can find one example (for "one-path next") of how a K rule is mapped to a reachability symbol, but for the others there isn't such a mapping given. In the bmc tests I can see that the #AG is used, but I can't seem to find other usages.
Are there any more documentation sources and/or K examples of how these reachability symbols can be used during verification? Or how they are (implicitly) used during verification?
| 13:10:21 |
| everett.hildenbrandt | Hmmmm, well as far as I know, we translate the reachability arrow in claims to #wEF (weak exists finally), but I may be incorrect on that. DKJPMGMS do you know?
The other symbols I think do not have immediate use, but we did have a temporal model checker for K called KBMC that used them. I think 7MM1DXE0 may know about that? Not sure. | 18:23:09 |
|  yi.zhang | 21:30:38 |
| yi.zhang | As far as I can remember, the semantics rules are translated into "one-path next" implications. reachablility claims are translated into either wEF or wAF implications. The haskell backend is capable of computing the all path next of a symbolic configuration. Together with some strategies, the haskell backend can be used to prove one-path/all-path reachablility claims. However, I don't think these reachability symbols explicitly appear in the execution of the haskell backend. In other words, the semantics of these symbols are hard-coded in the strategy implemented in the haskell backend. I think 7QGKQWE4 have some work on recovering the proof from the internal state of the haskell backend. In the proof, those symbol should reappear. | 21:30:39 |
 xiaohong.chen | The "one-path next" symbol captures one-step execution steps. It specifies the underlying transition relation of every K semantics. All the other operators such as AG wEF and wAF are definable using one-path next and least/greatest fixpoints operations. Unfortunately, iirc their concrete definitions are not to be found in Kore because Kore doesn't support specifications of fixpoints yet.
Given that said, there is documentation about these reachability symbols. For one-path reachability wEF see https://github.com/runtimeverification/haskell-backend/blob/master/docs/2018-11-08-One-Path-Reachability-Proofs.md. For all-path reachability wAF see https://github.com/runtimeverification/haskell-backend/blob/master/docs/2019-03-28-All-Path-Reachability-Proofs.md. These two reachability relations are used in verification. This paper (https://fsl.cs.illinois.edu/publications/stefanescu-park-yuwen-li-rosu-2016-oopsla.html) explains both of them and discusses the K verification algorithms. | 21:55:43 |
| 12 Jan 2023 |
 ana.pantilie95 | That's right, we only use those modalities to parse claims accordingly and the strategies themselves are hardcoded in the backend. | 11:13:59 |
| 13 Jan 2023 |
| Enzo Evers | Thank you for the information | 10:20:34 |
| 8ardamu | Hi all, we are looking for people with some experience in K.
Intern position in mechanized analysis of specifications
The IMDEA Software Institute invites applications for intern positions
on the mechanized formal analysis of rich specification for highly
critical software.
Industrial requirements for critical systems are often modeled in
temporal specification languages with clean semantics. The main goal
of the internship is to implement the formal operational semantics of
one concrete industrial specification language in a formal tool like
Maude, K or as a translation into formal modeling languages like
Alloy.
A second goal is to use the implementation of the operational
semantics to create tools that perform important tasks like
interpreters of the semantics, reachability queries (for example to be
used for automated test generation) or detects contradictions.
The ideal candidate should have a strong background in logic, automata
formal languages, and formal methods in general. Experience with tools
like Maude, K, TLA+ or Alloy is a plus.
Applications are invited to apply for a intern position at the IMDEA
Software Institute, Madrid, Spain.
Selected candidates will work with Pierre Ganty and Cesar Sanchez and
an international team of graduate students and researchers.
Who should apply?
Candidates should have a MSc or BSc degree (or be close to complete
one) in computer science, mathematics, or a related discipline, with
an interest in the above area, and a strong commitment to
research. Proven top programming skills as well as ability to
understand and develop algorithms are required. Good teamwork and
communication skills, including excellent spoken and written English
are also required.
Working at IMDEA Software
The position is based in Madrid, Spain, where the IMDEA Software
Institute is situated. The institute provides for travel expenses and
an internationally competitive stipend. The working language at the
IMDEA Software Institute is English.
Dates
The duration of the position will be at least 9 months.
How to apply?
Applicants interested in the position should submit their application
at https://careers.software.imdea.org/ using reference code
202301-mechspecs. Review of applications will begin immediately and
close when positions are filled or on February 15, 2023.
For enquiries about the position, please contact: pierre.ganty (at)
imdea.org or cesar.sanchez (at) imdea.org
| 10:41:11 |
|  Wei Tang (account deprecated, use @wei:parity.io for work and @wei:pacna.org for private) changed their display name from Wei Tang to Wei Tang (account deprecated, use @wei:parity.io for work and @wei:pacna.org for private). | 14:13:19 |
| 16 Jan 2023 |
|  @seanjohnstontips:matrix.org joined the room. | 12:15:46 |
| @seanjohnstontips:matrix.org set a profile picture. | 21:47:07 |
| 18 Jan 2023 |
| @seanjohnstontips:matrix.org left the room. | 06:16:07 |
| 24 Jan 2023 |
|  mehmetoguzderin changed their profile picture. | 21:16:40 |
| 27 Jan 2023 |
| mehmetoguzderin changed their profile picture. | 07:34:51 |
| 28 Jan 2023 |
|  playback2396 joined the room. | 09:54:31 |
| 2 Feb 2023 |
| mehmetoguzderin changed their profile picture. | 20:09:12 |
| mehmetoguzderin changed their profile picture. | 20:09:27 |
