konnov Follow

💭

having fun with @tlaplus, @tendermint, and apalache

Igor Konnov konnov

💭

having fun with @tlaplus, @tendermint, and apalache

research scientist at @informalsystems :: with @interchainio :: researcher at Inria Nancy :: postdoc at TU Wien :: Moscow State Univ. :: nil

Informal Systems
Vienna, Austria
Sign in to view email
https://konnov.github.io

Block or report user

Report or block konnov

Contact Support about this user’s behavior.

Learn more about reporting abuse

research scientist at @informalsystems :: with @interchainio :: researcher at Inria Nancy :: postdoc at TU Wien :: Moscow State Univ. :: nil

Informal Systems
Vienna, Austria
Sign in to view email
https://konnov.github.io

Block or report user

Report or block konnov

Contact Support about this user’s behavior.

Learn more about reporting abuse

Popular repositories

apalache

APALACHE: symbolic model checker for TLA+

Scala 122 4
bymc

Byzantine model checker

C 12 3
fault-tolerant-benchmarks

Fault-tolerant distributed algorithms encoded in a formal language

F* 9 3
apalache-tests

Benchmarks for apalache

SMT 2
apalache-blog

Using TLA+ and Apalache

1
konnov.github.io

Igor Konnov's page

505 contributions in the last year

Contribution activity

May 2020

konnov has no activity yet for this period.

April 2020

Tendermint safety and fork scenarios Apr 1

Unroll pass Apr 17
Ak/tlcconfig Apr 7

Add traceability tooling proposal Apr 1
Fastsync English Spec revision Apr 1

High level fast sync spec Apr 9

Created an issue in konnov/apalache that received 8 comments

A linter for TLA+

TLA+ as a language has a few annoying issues that could be found statically by using a set of simple rules. This could be done by implementing a si…

8 comments

Experiments for the new type inference Apr 28
Add incremental solver in ParModelChecker Apr 28
Optimize Z3SolverContext.toExpr and ConstSimplifierForSmt.simplifyDeep Apr 28
[FEATURE] PrettyWriter should extend the standard modules Apr 24
Manual: Explain the difference between bounded model checking and invariant checking Apr 21
[BUG] Unroller produces a recursive definition Apr 20
[BUG] Unroller produces stack overflow Apr 20
Unrolling recursive LET-IN definitions Apr 19
[FEATURE] Support for Bags Apr 17
[FEATURE] Do not inline nullary operators Apr 15
Prepare a manual on Apalache IR Apr 12
Update the manual on TLC counterexamples Apr 10
Update Apalache manual on TLC config files Apr 10
Refactor topological sort of definitions Apr 10
[FEATURE] JSON importer Apr 8

You can’t perform that action at this time.