The K Framework User Group

210 Members
The K Framework (kframework.org) and its applications to smart contracts.  EVM: github.com/kframework/evm-semantics Viper: github.com/kframework/viper-semantics44 Servers

Load older messages

2 Jul 2020
@matthewfl:matrix.orgmatthewflis there a manual that complete and up to date that specs everything out that I should be looking at, or is it mostly just documentation attached to the various tutorials?15:37:42
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt We have the pending documentation here which we add to on an as-asked-for basis: https://github.com/kframework/k/blob/master/pending-documentation.md 15:45:19
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt So if there is a feature you find is not documented there, you can open an issue and we'll add documentation. 15:45:35
5 Jul 2020
@egeas:asra.gregeas 09:02:16
6 Jul 2020
@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort I'm having issues getting a proof through with the following causing failure:
  #Ceil ( _M [ K <- V ] )                                                                                                                                                             
  #Ceil ( _M [ K <- V ] [ K ] )                                 
  #Not ( {                                                                                                                                                                            
    _M [ K <- V ] [ K ]                                                                                                                                                           
  } )                                                                                                                                                                                                                                                               
I'm trying to force this one through by adding the following, but it's not helping:
    rule M:Map [ K  - V ] [ K ] =  V [simplification]
@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort Any ideas? 17:09:19
7 Jul 2020
@cerys7003:matrix.org@cerys7003:matrix.org joined the room.17:38:52
@sesh:feneas.orgsesh 21:13:58
8 Jul 2020
@cerys7003:matrix.org@cerys7003:matrix.org left the room.00:58:03
@chexxor_web:matrix.orgchexxor joined the room.19:36:28
@chexxor:matrix.orgchexxor joined the room.19:38:27

I'm interested in using the K framework project in a future project -- I want to do static analysis of the business logic built on top of a database, composed of multiple languages.

Does this sound like an appropriate application of the K project?

@chexxor:matrix.orgchexxorAlso, I am guessing that a temporal logic checker, like I hear TLA+ has, would be useful for cross-transaction analysis. Does K Platform do temporal analysis? Or anything like it?20:03:41
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Depends on the type of analysis you want to perform. To be clear, K is not for static analysis, though you can achieve the same results, but K does dynamic (or runtime) analysis/verification. 20:04:09
@chexxor:matrix.orgchexxor Is your definition of static analysis basically "what's the cyclomatic complexity of this code"? Or something more general? 20:05:21
@chexxor:matrix.orgchexxor I want to do something akin to "type checking" across the languages, which sounds like static analysis to me, a layperson. 20:06:11
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Well, my definition of static analysis is the general technique of analyzing code statically, abstracting parts of it, and inferring specific things about the code from that abstracted version. 20:06:24
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Type checking can be done statically using abstraction (normal way) or dynamically by executing a program to its type (how we normally approach it in K). 20:06:56
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt K can do some temporal model checking. It has built-in support for any reachability queries (which encompasses correctness and safety properties) - think of the "All-path Eventually" fragment of most temporal logics. We also have pretty simple/standard ways of encoding temporal properties as reachability queries, but don't have built-in support for them. 20:11:54
@chexxor:matrix.orgchexxorOk, that answers my question for now! It gives me some new things to read and learn, also! Thank you for your help!20:19:56
@rose0525570:matrix.org@rose0525570:matrix.org joined the room.23:59:03
9 Jul 2020
@demi390600:matrix.org@demi390600:matrix.org joined the room.01:34:18
@demi390600:matrix.org@demi390600:matrix.org left the room.02:33:16
@rose0525570:matrix.org@rose0525570:matrix.org left the room.03:52:05
@martina:tchncs.demartina 20:28:04
@sharma:diasp.insharma 20:42:09
10 Jul 2020
@kermit:kde.orgkermit 19:24:14
12 Jul 2020
@hackphobia:matrix.orghackphobic changed their display name from hackphobia to hackphobic.08:30:50
13 Jul 2020
@matthewfl:matrix.orgmatthewflIn the pending documentation, it says "where isPrime(_) is a predicate that can be defined in the usual way." is the way to define new predicates documented?16:56:46
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Well they're just functions defined in sort Bool:
syntax Bool ::= isPrime ( Int ) [function]

rule isPrime(1) => false
rule isPrime(2) => true

There are no newer messages yet.

Back to Room List