-
Notifications
You must be signed in to change notification settings - Fork 41
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Proof Refactoring #671
Proof Refactoring #671
Commits on Nov 27, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 60055de - Browse repository at this point
Copy the full SHA 60055deView commit details -
Configuration menu - View commit details
-
Copy full SHA for a30dbb1 - Browse repository at this point
Copy the full SHA a30dbb1View commit details -
Configuration menu - View commit details
-
Copy full SHA for d72b396 - Browse repository at this point
Copy the full SHA d72b396View commit details
Commits on Nov 28, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 62f36a9 - Browse repository at this point
Copy the full SHA 62f36a9View commit details -
Configuration menu - View commit details
-
Copy full SHA for c5a3332 - Browse repository at this point
Copy the full SHA c5a3332View commit details
Commits on Nov 29, 2023
-
cherry-pick Floyd-Hoare changes from wip/dk/empire-owicki
These changes allow computing Floyd/Hoare annotations for product automata of concurrent programs.
Configuration menu - View commit details
-
Copy full SHA for 76a50a2 - Browse repository at this point
Copy the full SHA 76a50a2View commit details -
Configuration menu - View commit details
-
Copy full SHA for 2c4dc82 - Browse repository at this point
Copy the full SHA 2c4dc82View commit details -
BasicCegarLoop should not refer to Floyd/Hoare proofs, let NwaCegarLoop handle this. Also, CEGAR loops refer directly to Hoare annotation states, not IcfgLocations.
Configuration menu - View commit details
-
Copy full SHA for a87a7c0 - Browse repository at this point
Copy the full SHA a87a7c0View commit details -
HoareAnnotationFragments: rely on supplied hoareAnnotationStates
Do not check the setting again, the caller should supply the appropriate states.
Configuration menu - View commit details
-
Copy full SHA for 224148a - Browse repository at this point
Copy the full SHA 224148aView commit details -
move HoareAnnotationPositions to its own file
Also define their semantics in the class itself, rather than in some utility class.
Configuration menu - View commit details
-
Copy full SHA for 0cd9943 - Browse repository at this point
Copy the full SHA 0cd9943View commit details -
Configuration menu - View commit details
-
Copy full SHA for c9454fe - Browse repository at this point
Copy the full SHA c9454feView commit details -
Configuration menu - View commit details
-
Copy full SHA for c3557f2 - Browse repository at this point
Copy the full SHA c3557f2View commit details -
Configuration menu - View commit details
-
Copy full SHA for 94a263c - Browse repository at this point
Copy the full SHA 94a263cView commit details
Commits on Nov 30, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 05c0479 - Browse repository at this point
Copy the full SHA 05c0479View commit details -
Configuration menu - View commit details
-
Copy full SHA for 87eb079 - Browse repository at this point
Copy the full SHA 87eb079View commit details -
Configuration menu - View commit details
-
Copy full SHA for 3f177bc - Browse repository at this point
Copy the full SHA 3f177bcView commit details -
Configuration menu - View commit details
-
Copy full SHA for 276e2b5 - Browse repository at this point
Copy the full SHA 276e2b5View commit details -
Configuration menu - View commit details
-
Copy full SHA for d17f6f0 - Browse repository at this point
Copy the full SHA d17f6f0View commit details
Commits on Dec 1, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 1604cae - Browse repository at this point
Copy the full SHA 1604caeView commit details -
Configuration menu - View commit details
-
Copy full SHA for 6f4c56b - Browse repository at this point
Copy the full SHA 6f4c56bView commit details -
Configuration menu - View commit details
-
Copy full SHA for f2110d5 - Browse repository at this point
Copy the full SHA f2110d5View commit details -
Configuration menu - View commit details
-
Copy full SHA for eea7867 - Browse repository at this point
Copy the full SHA eea7867View commit details
Commits on Dec 2, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 2032d1f - Browse repository at this point
Copy the full SHA 2032d1fView commit details
Commits on Dec 3, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 54d3723 - Browse repository at this point
Copy the full SHA 54d3723View commit details
Commits on Dec 12, 2023
-
Configuration menu - View commit details
-
Copy full SHA for b4501bd - Browse repository at this point
Copy the full SHA b4501bdView commit details -
Configuration menu - View commit details
-
Copy full SHA for b37babc - Browse repository at this point
Copy the full SHA b37babcView commit details
Commits on Dec 14, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 9080e3b - Browse repository at this point
Copy the full SHA 9080e3bView commit details -
Configuration menu - View commit details
-
Copy full SHA for eb2b75c - Browse repository at this point
Copy the full SHA eb2b75cView commit details
Commits on Dec 15, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 87b555a - Browse repository at this point
Copy the full SHA 87b555aView commit details
Commits on Dec 17, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 0aaec9c - Browse repository at this point
Copy the full SHA 0aaec9cView commit details -
Configuration menu - View commit details
-
Copy full SHA for f62a22f - Browse repository at this point
Copy the full SHA f62a22fView commit details -
Configuration menu - View commit details
-
Copy full SHA for 2c18645 - Browse repository at this point
Copy the full SHA 2c18645View commit details -
Configuration menu - View commit details
-
Copy full SHA for 2bbf6a2 - Browse repository at this point
Copy the full SHA 2bbf6a2View commit details -
Configuration menu - View commit details
-
Copy full SHA for 92aeb31 - Browse repository at this point
Copy the full SHA 92aeb31View commit details -
Configuration menu - View commit details
-
Copy full SHA for 6f6212a - Browse repository at this point
Copy the full SHA 6f6212aView commit details -
Configuration menu - View commit details
-
Copy full SHA for 646c763 - Browse repository at this point
Copy the full SHA 646c763View commit details -
Configuration menu - View commit details
-
Copy full SHA for d48c12e - Browse repository at this point
Copy the full SHA d48c12eView commit details
Commits on Dec 18, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 982513e - Browse repository at this point
Copy the full SHA 982513eView commit details
Commits on Dec 20, 2023
-
Configuration menu - View commit details
-
Copy full SHA for a7c5404 - Browse repository at this point
Copy the full SHA a7c5404View commit details -
Configuration menu - View commit details
-
Copy full SHA for 177732a - Browse repository at this point
Copy the full SHA 177732aView commit details -
Configuration menu - View commit details
-
Copy full SHA for ed90216 - Browse repository at this point
Copy the full SHA ed90216View commit details
Commits on Dec 21, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 50509a4 - Browse repository at this point
Copy the full SHA 50509a4View commit details -
Configuration menu - View commit details
-
Copy full SHA for ffa4bff - Browse repository at this point
Copy the full SHA ffa4bffView commit details -
Configuration menu - View commit details
-
Copy full SHA for aa874c3 - Browse repository at this point
Copy the full SHA aa874c3View commit details -
Configuration menu - View commit details
-
Copy full SHA for 66b37b6 - Browse repository at this point
Copy the full SHA 66b37b6View commit details -
Configuration menu - View commit details
-
Copy full SHA for 5a53242 - Browse repository at this point
Copy the full SHA 5a53242View commit details -
Configuration menu - View commit details
-
Copy full SHA for 38d3fd1 - Browse repository at this point
Copy the full SHA 38d3fd1View commit details
Commits on Dec 22, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 6f0885e - Browse repository at this point
Copy the full SHA 6f0885eView commit details -
Configuration menu - View commit details
-
Copy full SHA for c943d41 - Browse repository at this point
Copy the full SHA c943d41View commit details -
Configuration menu - View commit details
-
Copy full SHA for c9b4873 - Browse repository at this point
Copy the full SHA c9b4873View commit details -
Configuration menu - View commit details
-
Copy full SHA for d1c4f2c - Browse repository at this point
Copy the full SHA d1c4f2cView commit details
Commits on Feb 4, 2024
-
Merge branch 'dev' into wip/dk/proof-refactoring
# Conflicts: # trunk/source/InvariantSynthesis/src/de/uni_freiburg/informatik/ultimate/plugins/generator/invariantsynthesis/InvariantSynthesisStarter.java # trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/smt/predicates/PredicateUtils.java # trunk/source/Library-Proofs/src/de/uni_freiburg/informatik/ultimate/lib/proofs/floydhoare/HoareAnnotationComposer.java # trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/TraceAbstractionStarter.java # trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/TraceAbstractionUtils.java # trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/predicates/HoareAnnotationChecker.java
Configuration menu - View commit details
-
Copy full SHA for 26b3c0d - Browse repository at this point
Copy the full SHA 26b3c0dView commit details -
Configuration menu - View commit details
-
Copy full SHA for a67f538 - Browse repository at this point
Copy the full SHA a67f538View commit details -
Configuration menu - View commit details
-
Copy full SHA for a1f6fff - Browse repository at this point
Copy the full SHA a1f6fffView commit details -
Configuration menu - View commit details
-
Copy full SHA for 6d4caa8 - Browse repository at this point
Copy the full SHA 6d4caa8View commit details -
Configuration menu - View commit details
-
Copy full SHA for 098a0b3 - Browse repository at this point
Copy the full SHA 098a0b3View commit details -
Configuration menu - View commit details
-
Copy full SHA for 7b35f9c - Browse repository at this point
Copy the full SHA 7b35f9cView commit details -
Configuration menu - View commit details
-
Copy full SHA for 806e1ff - Browse repository at this point
Copy the full SHA 806e1ffView commit details -
Configuration menu - View commit details
-
Copy full SHA for 38790be - Browse repository at this point
Copy the full SHA 38790beView commit details -
Configuration menu - View commit details
-
Copy full SHA for 18f2a4f - Browse repository at this point
Copy the full SHA 18f2a4fView commit details -
Configuration menu - View commit details
-
Copy full SHA for f43013b - Browse repository at this point
Copy the full SHA f43013bView commit details
Commits on Feb 5, 2024
-
separate proof production from postprocessing
CEGAR loops decide which kinds of proofs they provide and how. Disentangle possible postprocessing of proofs from CEGAR loops and proof production.
Configuration menu - View commit details
-
Copy full SHA for a5e34d2 - Browse repository at this point
Copy the full SHA a5e34d2View commit details
Commits on Feb 9, 2024
-
Configuration menu - View commit details
-
Copy full SHA for d3528af - Browse repository at this point
Copy the full SHA d3528afView commit details
Commits on Aug 8, 2024
-
Merge branch 'dev' into wip/dk/proof-refactoring
# Conflicts: # trunk/source/InvariantSynthesis/src/de/uni_freiburg/informatik/ultimate/plugins/generator/invariantsynthesis/InvariantSynthesisStarter.java # trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/smt/predicates/PredicateUtils.java # trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/TraceAbstractionStarter.java
Configuration menu - View commit details
-
Copy full SHA for 65dc64b - Browse repository at this point
Copy the full SHA 65dc64bView commit details -
Configuration menu - View commit details
-
Copy full SHA for 00854ba - Browse repository at this point
Copy the full SHA 00854baView commit details -
Configuration menu - View commit details
-
Copy full SHA for be8f228 - Browse repository at this point
Copy the full SHA be8f228View commit details -
Configuration menu - View commit details
-
Copy full SHA for bbace90 - Browse repository at this point
Copy the full SHA bbace90View commit details -
Configuration menu - View commit details
-
Copy full SHA for 05361c4 - Browse repository at this point
Copy the full SHA 05361c4View commit details -
Configuration menu - View commit details
-
Copy full SHA for c6c3409 - Browse repository at this point
Copy the full SHA c6c3409View commit details -
Configuration menu - View commit details
-
Copy full SHA for 6ac7e5e - Browse repository at this point
Copy the full SHA 6ac7e5eView commit details -
continue refactoring; major simplifications
- introduce marker interface IProof to avoid using Object - decouple AbstractCegarLoop, CegarLoopResult from proof production - remove useless interfaces - decouple proofs and proof translation from IInitialAbstractionProvider interface
Configuration menu - View commit details
-
Copy full SHA for be80620 - Browse repository at this point
Copy the full SHA be80620View commit details
Commits on Aug 9, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 1083d51 - Browse repository at this point
Copy the full SHA 1083d51View commit details -
Configuration menu - View commit details
-
Copy full SHA for 766c9b2 - Browse repository at this point
Copy the full SHA 766c9b2View commit details -
Configuration menu - View commit details
-
Copy full SHA for 7c30132 - Browse repository at this point
Copy the full SHA 7c30132View commit details -
Configuration menu - View commit details
-
Copy full SHA for e56112c - Browse repository at this point
Copy the full SHA e56112cView commit details -
AbstractBuchiCegarLoop: precondition of interpolant automaton is not …
…necessarily "true"
Configuration menu - View commit details
-
Copy full SHA for 260f8f7 - Browse repository at this point
Copy the full SHA 260f8f7View commit details -
Configuration menu - View commit details
-
Copy full SHA for 42e75cd - Browse repository at this point
Copy the full SHA 42e75cdView commit details -
Configuration menu - View commit details
-
Copy full SHA for c866311 - Browse repository at this point
Copy the full SHA c866311View commit details -
Configuration menu - View commit details
-
Copy full SHA for c42ea25 - Browse repository at this point
Copy the full SHA c42ea25View commit details -
Configuration menu - View commit details
-
Copy full SHA for 4355d7b - Browse repository at this point
Copy the full SHA 4355d7bView commit details
Commits on Aug 10, 2024
-
Configuration menu - View commit details
-
Copy full SHA for f5d630e - Browse repository at this point
Copy the full SHA f5d630eView commit details -
contract computation: requires may be needed even if ensures is null …
…to prove asserts inside the procedure
Configuration menu - View commit details
-
Copy full SHA for 9ddd293 - Browse repository at this point
Copy the full SHA 9ddd293View commit details
Commits on Aug 11, 2024
-
Configuration menu - View commit details
-
Copy full SHA for a77894b - Browse repository at this point
Copy the full SHA a77894bView commit details
Commits on Aug 12, 2024
-
Configuration menu - View commit details
-
Copy full SHA for ccca8fe - Browse repository at this point
Copy the full SHA ccca8feView commit details -
Configuration menu - View commit details
-
Copy full SHA for 1e57a53 - Browse repository at this point
Copy the full SHA 1e57a53View commit details
Commits on Aug 14, 2024
-
Merge branch 'dev' into wip/dk/proof-refactoring
Removes the workaround introduced in 720a012, as proofs of different CEGAR loops are now stored separately in the ICFG. # Conflicts: # trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/NwaCegarLoop.java
Configuration menu - View commit details
-
Copy full SHA for 122fb1c - Browse repository at this point
Copy the full SHA 122fb1cView commit details
Commits on Aug 15, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 2b4fdb3 - Browse repository at this point
Copy the full SHA 2b4fdb3View commit details -
Configuration menu - View commit details
-
Copy full SHA for 053cbaa - Browse repository at this point
Copy the full SHA 053cbaaView commit details -
add explicit representations of the specification shown by a proof
This is particularly useful if we create multiple proof objects for the same program and different (partial) specifications, to distinguish which proof objects relate to which specification.
Configuration menu - View commit details
-
Copy full SHA for 9007b66 - Browse repository at this point
Copy the full SHA 9007b66View commit details
Commits on Aug 16, 2024
-
Configuration menu - View commit details
-
Copy full SHA for a2c4c3b - Browse repository at this point
Copy the full SHA a2c4c3bView commit details -
Configuration menu - View commit details
-
Copy full SHA for 591e8a7 - Browse repository at this point
Copy the full SHA 591e8a7View commit details
Commits on Aug 17, 2024
-
fix block encoding bug discovered by contract computation
Every procedure that exists in the IIcfg should have an exit location, even if that location is unreachable. This was not the case for the IIcfgs produced by the BlockEncodingV2 plugin. This commit fixes this bug, and introduces an assert statement after block encoding has finished to check if the produced IIcfg satisfies this invariant. Moreover, we add two sanity checks regarding the computation of procedure contracts, where the problem was discovered (the location of the ProcedureContractResult was null), such that similar issues are caught earlier in the future.
Configuration menu - View commit details
-
Copy full SHA for 32bd4b9 - Browse repository at this point
Copy the full SHA 32bd4b9View commit details
Commits on Aug 18, 2024
-
Merge branch 'dev' into wip/dk/proof-refactoring
# Conflicts: # trunk/source/InvariantSynthesis/src/de/uni_freiburg/informatik/ultimate/plugins/generator/invariantsynthesis/InvariantSynthesisStarter.java # trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/smt/predicates/HoareAnnotation.java # trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/smt/predicates/PredicateFactory.java # trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/HoareAnnotationWriter.java
Configuration menu - View commit details
-
Copy full SHA for 9d7a9aa - Browse repository at this point
Copy the full SHA 9d7a9aaView commit details
Commits on Aug 19, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 6679c7b - Browse repository at this point
Copy the full SHA 6679c7bView commit details
Commits on Aug 20, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 044eca1 - Browse repository at this point
Copy the full SHA 044eca1View commit details -
Merge branch 'dev' into wip/dk/proof-refactoring
# Conflicts: # releaseScripts/website-config/frontend/config.js # trunk/source/WebsiteStatic/config/config.dist.js
Configuration menu - View commit details
-
Copy full SHA for b03ad22 - Browse repository at this point
Copy the full SHA b03ad22View commit details -
Configuration menu - View commit details
-
Copy full SHA for 5f48c28 - Browse repository at this point
Copy the full SHA 5f48c28View commit details