No abstract available.
Cited By
- Zhang L, Zilberstein N, Kaminski B and Silva A (2024). Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers, Proceedings of the ACM on Programming Languages, 8:OOPSLA2, (817-845), Online publication date: 8-Oct-2024.
- Cornejo C, Regis G, Aguirre N and Frias M (2023). A Study of the Electrum and DynAlloy Dynamic Behavior Notations, IEEE Transactions on Software Engineering, 49:11, (4946-4963), Online publication date: 1-Nov-2023.
- Hirsch R and Šemrl J Demonic lattices and semilattices in relational semigroups with ordinary composition Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, (1-10)
- Warford J, Vega D and Staley S (2020). A Calculational Deductive System for Linear Temporal Logic, ACM Computing Surveys, 53:3, (1-38), Online publication date: 31-May-2021.
- Liu Y, Li Y, Lin S and Zhao R Towards automated verification of smart contract fairness Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, (666-677)
- Jacobs B (2019). The mathematics of changing one's mind, via Jeffrey's or via Pearl's update rule, Journal of Artificial Intelligence Research, 65:1, (783-806), Online publication date: 1-May-2019.
- Lin S, Sun J, Xiao H, Liu Y, Sanán D and Hansen H FiB: squeezing loop invariants by interpolation between Forward/Backward predicate transformers Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, (793-803)
- Regis G, Cornejo C, Gutiérrez Brida S, Politano M, Raverta F, Ponzio P, Aguirre N, Galeotti J and Frias M DynAlloy analyzer: a tool for the specification and analysis of alloy models with dynamic behaviour Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, (969-973)
- Chaudhari D and Damani O (2017). Assumption propagation through annotated programs, Formal Aspects of Computing, 29:3, (495-530), Online publication date: 1-May-2017.
- Khedri R, Jones O and Alabbad M Defense in Depth Formulation and Usage in Dynamic Access Control Proceedings of the 6th International Conference on Principles of Security and Trust - Volume 10204, (253-274)
- Mastroeni I and Zanardini D (2017). Abstract Program Slicing, ACM Transactions on Computational Logic, 18:1, (1-58), Online publication date: 31-Jan-2017.
- You Z, Xue J and Zuo Z (2016). Unified formal derivation and automatic verification of three binary-tree traversal non-recursive algorithms, Cluster Computing, 19:4, (2145-2156), Online publication date: 1-Dec-2016.
- Hudon S, Hoang T and Ostroff J (2016). The Unit-B method, Software and Systems Modeling (SoSyM), 15:4, (1091-1116), Online publication date: 1-Oct-2016.
- (2016). A formalization of programs in first-order logic with a discrete linear order, Artificial Intelligence, 235:C, (1-25), Online publication date: 1-Jun-2016.
- Belo Lourenço C, Frade M and Sousa Pinto J Formalizing Single-Assignment Program Verification Proceedings of the 25th European Symposium on Programming Languages and Systems - Volume 9632, (41-67)
- Namjoshi K and Trefler R Parameterized Compositional Model Checking Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9636, (589-606)
- Namjoshi K and Trefler R Analysis of Dynamic Process Networks Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9035, (164-178)
- Cousot P Abstracting Induction by Extrapolation and Interpolation Proceedings of the 16th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 8931, (19-42)
- Aichernig B, Jöbstl E and Tiran S (2015). Model-based mutation testing via symbolic refinement checking, Science of Computer Programming, 97:P4, (383-404), Online publication date: 1-Jan-2015.
- Mendes A, Backhouse R and Ferreira J Structure Editing of Handwritten Mathematics Proceedings of the Ninth ACM International Conference on Interactive Tabletops and Surfaces, (139-148)
- Hawkins R, Miyazawa A, Cavalcanti A, Kelly T and Rowlands J Assurance Cases for Block-Configurable Software Proceedings of the 33rd International Conference on Computer Safety, Reliability, and Security - Volume 8666, (155-169)
- Lin F A formalization of programs in first-order logic with a discrete linear order Proceedings of the Fourteenth International Conference on Principles of Knowledge Representation and Reasoning, (338-347)
- Hallerstede S Quasi-Lexicographic Convergence Proceedings of the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z - Volume 8477, (86-100)
- Dong R, Faber J, Ke W and Liu Z rCOS Unifying Theories of Programming and Formal Engineering Methods, (1-66)
- Leino K and Polikarpova N Verified Calculations Revised Selected Papers of the 5th International Conference on Verified Software: Theories, Tools, Experiments - Volume 8164, (170-190)
- Mosbahi O (2013). Combining Formal Methods for the Development of Reactive Systems, ACM Transactions on Embedded Computing Systems, 12:1, (1-29), Online publication date: 1-Jan-2013.
- Kanig J, Schonberg E and Dross C Hi-Lite Proceedings of the 2012 ACM conference on High integrity language technology, (27-34)
- Kanig J, Schonberg E and Dross C (2012). Hi-Lite, ACM SIGAda Ada Letters, 32:3, (27-34), Online publication date: 29-Nov-2012.
- Barbosa L and Martinho M Mathematical Literacy as a Condition for Sustainable Development Revised Selected Papers of the SEFM 2012 Satellite Events on Information Technology and Open Source: Applications for Education, Innovation, and Sustainability - Volume 7991, (64-77)
- Morgan C Elementary probability theory in the eindhoven style Proceedings of the 11th international conference on Mathematics of Program Construction, (48-73)
- Namjoshi K and Trefler R Local symmetry and compositional verification Proceedings of the 13th international conference on Verification, Model Checking, and Abstract Interpretation, (348-362)
- Fahrenberg U, Legay A and Wasowski A Vision paper Proceedings of the 14th international conference on Model driven engineering languages and systems, (490-500)
- Ferreira J, Mendes A, Cunha A, Baquero C, Silva P, Barbosa L and Oliveira J Logic training through algorithmic problem solving Proceedings of the Third international congress conference on Tools for teaching logic, (62-69)
- Zheng Y, Shi H and Xue J A knowledge-driven approach to web-based learning for formal algorithm development Proceedings of the 2010 international conference on New horizons in web-based learning, (237-245)
- Čaušević A, Seceleanu C and Pettersson P Modeling and reasoning about service behaviors and their compositions Proceedings of the 4th international conference on Leveraging applications of formal methods, verification, and validation - Volume Part II, (82-96)
- Cohen A, Namjoshi K, Sa'ar Y, Zuck L and Kisyova K Parallelizing a symbolic compositional model-checking algorithm Proceedings of the 6th international conference on Hardware and software: verification and testing, (46-59)
- Dell'Aquila C, Di Tria F, Lefons E and Tangorra F Logic programming for data warehouse conceptual schema validation Proceedings of the 12th international conference on Data warehousing and knowledge discovery, (1-12)
- Cohen A, Namjoshi K and Sa'ar Y A dash of fairness for compositional reasoning Proceedings of the 22nd international conference on Computer Aided Verification, (543-557)
- Hayes I, Dunne S and Meinicke L Unifying theories of programming that distinguish nontermination and abort Proceedings of the 10th international conference on Mathematics of program construction, (178-194)
- Srivastava S, Gulwani S and Foster J From program verification to program synthesis Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (313-326)
- Srivastava S, Gulwani S and Foster J (2010). From program verification to program synthesis, ACM SIGPLAN Notices, 45:1, (313-326), Online publication date: 2-Jan-2010.
- Dunne S (2009). Of wlp and CSP, Electronic Notes in Theoretical Computer Science (ENTCS), 259, (35-45), Online publication date: 1-Dec-2009.
- Cook B, Podelski A and Rybalchenko A (2009). Summarization for termination, Formal Methods in System Design, 35:3, (369-387), Online publication date: 1-Dec-2009.
- Krenn W and Aichernig B (2009). Test Case Generation by Contract Mutation in Spec#, Electronic Notes in Theoretical Computer Science (ENTCS), 253:2, (71-86), Online publication date: 1-Oct-2009.
- Blanco J, Losano L, Aguirre N, Novaira M, Permigiani S and Scilingo G (2009). An introductory course on programming based on formal specification and program calculation, ACM SIGCSE Bulletin, 41:2, (31-37), Online publication date: 25-Jun-2009.
- Morris J, Bunkenburg A and Tyrrell M (2009). Term transformers, ACM Transactions on Programming Languages and Systems, 31:4, (1-42), Online publication date: 1-May-2009.
- Cohen A and Namjoshi K (2009). Local proofs for global safety properties, Formal Methods in System Design, 34:2, (104-125), Online publication date: 1-Apr-2009.
- Hughes J and Jones C (2008). Reasoning about programs via operational semantics, Automated Software Engineering, 15:3-4, (299-312), Online publication date: 1-Dec-2008.
- Demirbas M and Arora A An Application of Specification-Based Design of Self-stabilization to Tracking in Wireless Sensor Networks Proceedings of the 10th International Symposium on Stabilization, Safety, and Security of Distributed Systems, (203-217)
- Samanta R, Deshmukh J and Emerson E Automatic generation of local repairs for Boolean programs Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, (1-10)
- Dunne S, Hayes I and Galloway A Reasoning about loops in total and general correctness Proceedings of the 2nd international conference on Unifying theories of programming, (62-81)
- Meinicke L and Hayes I Probabilistic Choice in Refinement Algebra Proceedings of the 9th international conference on Mathematics of Program Construction, (243-267)
- Cook B, Gulwani S, Lev-Ami T, Rybalchenko A and Sagiv M Proving Conditional Termination Proceedings of the 20th international conference on Computer Aided Verification, (328-340)
- Cohen A and Namjoshi K Local Proofs for Linear-Time Properties of Concurrent Programs Proceedings of the 20th international conference on Computer Aided Verification, (149-161)
- Babic D and Hu A Calysto Proceedings of the 30th international conference on Software engineering, (211-220)
- Rocha C and Meseguer J Theorem proving modulo based on Boolean equational procedures Proceedings of the 10th international conference on Relational and kleene algebra methods in computer science, and 5th international conference on Applications of kleene algebra, (337-351)
- Frias M, Lopez Pombo C, Galeotti J and Aguirre N (2007). Efficient Analysis of DynAlloy Specifications, ACM Transactions on Software Engineering and Methodology, 17:1, (1-34), Online publication date: 1-Dec-2007.
- Back R, Mannila L, Peltomäki M and Salakoski T Improving mathematics and programming education Proceedings of the Seventh Baltic Sea Conference on Computing Education Research - Volume 88, (167-170)
- Babić D and Hu A Exploiting shared structure in software verification conditions Proceedings of the 3rd international Haifa verification conference on Hardware and software: verification and testing, (169-184)
- van Leeuwen A (2007). Building Verification Condition Generators by Compositional Extension, Electronic Notes in Theoretical Computer Science (ENTCS), 191, (73-83), Online publication date: 1-Oct-2007.
- Barsotti D and Blanco J Automatic refinement of split binary semaphore Proceedings of the 4th international conference on Theoretical aspects of computing, (64-78)
- Babic D and Hu A Structural abstraction of software verification conditions Proceedings of the 19th international conference on Computer aided verification, (366-378)
- Cohen A and Namjoshi K Local proofs for global safety properties Proceedings of the 19th international conference on Computer aided verification, (55-67)
- Dunne S and Galloway A Lifting general correctness into partial correctness is ok Proceedings of the 6th international conference on Integrated formal methods, (215-232)
- Sivilotti P and Pike S (2007). A collection of kinesthetic learning activities for a course on distributed computing, ACM SIGACT News, 38:2, (56-74), Online publication date: 1-Jun-2007.
- Namjoshi K Symmetry and completeness in the analysis of parameterized systems Proceedings of the 8th international conference on Verification, model checking, and abstract interpretation, (299-313)
- Habel A, Pennemann K and Rensink A Weakest preconditions for high-level programs Proceedings of the Third international conference on Graph Transformations, (445-460)
- Fidge C (2006). Formal change impact analyses for emulated control software, International Journal on Software Tools for Technology Transfer (STTT), 8:4-5, (321-335), Online publication date: 1-Aug-2006.
- Martin C and Curtis S Nondeterministic folds Proceedings of the 8th international conference on Mathematics of Program Construction, (274-298)
- Nesterenko M and Tixeuil S Discovering network topology in the presence of byzantine faults Proceedings of the 13th international conference on Structural Information and Communication Complexity, (212-226)
- Boute R (2006). Calculational semantics, ACM Transactions on Programming Languages and Systems, 28:4, (747-793), Online publication date: 1-Jul-2006.
- Charpentier M (2006). Composing invariants, Science of Computer Programming, 60:3, (221-243), Online publication date: 1-May-2006.
- Arora A, Kulkarni S and Demirbas M (2006). Resettable vector clocks, Journal of Parallel and Distributed Computing, 66:2, (221-237), Online publication date: 1-Feb-2006.
- Lermer K, Fidge C and Hayes I (2005). A theory for execution-time derivation in real-time programs, Theoretical Computer Science, 346:1, (3-27), Online publication date: 23-Nov-2005.
- Frias M, López Pombo C, Baum G, Aguirre N and Maibaum T (2005). Reasoning about static and dynamic properties in alloy, ACM Transactions on Software Engineering and Methodology, 14:4, (478-526), Online publication date: 1-Oct-2005.
- Prasetya I, Azurat A, Vos T and Van Leeuwen A Building Verification Condition Generators by Compositional Extensions Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, (220-230)
- Frias M, Galeotti J, López Pombo C and Aguirre N DynAlloy Proceedings of the 27th international conference on Software engineering, (442-451)
- Leavens G, Cheon Y, Clifton C, Ruby C and Cok D (2005). How the design of JML accommodates both runtime assertion checking and formal verification, Science of Computer Programming, 55:1-3, (185-208), Online publication date: 1-Mar-2005.
- Zhang Y and Xu B (2004). A survey of semantic description frameworks for programming languages, ACM SIGPLAN Notices, 39:3, (14-30), Online publication date: 1-Mar-2004.
- Powell D Automatic derivation of loop termination conditions to support verification Proceedings of the 27th Australasian conference on Computer science - Volume 26, (89-97)
- Teng G and Liu X Support software evolution with abstration rules and programming knowledge patterns Focus on computational neurobiology, (177-189)
- Bozga M, Iosif R and Laknech Y (2003). Storeless semantics and alias logic, ACM SIGPLAN Notices, 38:10, (55-65), Online publication date: 1-Oct-2003.
- Bozga M, Iosif R and Laknech Y Storeless semantics and alias logic Proceedings of the 2003 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation, (55-65)
- Dunne S Introducing backward refinement into B Proceedings of the 3rd international conference on Formal specification and development in Z and B, (178-196)
- Leino K A SAT characterization of boolean-program correctness Proceedings of the 10th international conference on Model checking software, (104-120)
- Jones C (2003). The Early Search for Tractable Ways of Reasoning about Programs, IEEE Annals of the History of Computing, 25:2, (26-49), Online publication date: 1-Apr-2003.
- Smith S and Talcott C (2002). Specification Diagrams for Actor Systems, Higher-Order and Symbolic Computation, 15:4, (301-348), Online publication date: 1-Dec-2002.
- Sobel A and Clarkson M (2002). Formal Methods Application, IEEE Transactions on Software Engineering, 28:3, (308-320), Online publication date: 1-Mar-2002.
- von Karger B Temporal algebra Algebraic and coalgebraic methods in the mathematics of program construction, (309-385)
- Backhouse R Galois connections and fixed point calculus Algebraic and coalgebraic methods in the mathematics of program construction, (89-148)
- Arora A, Demirbas M and Kulkarniy S Graybox Stabilization Proceedings of the 2001 International Conference on Dependable Systems and Networks (formerly: FTCS), (389-400)
- Doherty P, Łukaszewicz W and Madalińska-Bugaj E (2000). The PMA and Relativizing Minimal Change for Action Update, Fundamenta Informaticae, 44:1-2, (95-131), Online publication date: 15-Aug-2000.
- Arora A, Kulkarni S and Demirbas M Resettable vector clocks Proceedings of the nineteenth annual ACM symposium on Principles of distributed computing, (269-278)
- Boute R (2000). Supertotal Function Definition in Mathematics and Software Engineering, IEEE Transactions on Software Engineering, 26:7, (662-672), Online publication date: 1-Jul-2000.
- Stevenson D Exploring an information-based approach to computation and computational complexity Proceedings of the 38th annual ACM Southeast Conference, (42-50)
- Doherty P, Łukaszewicz W and Madalińska-Bugaj E (2000). The PMA and Relativizing Minimal Change for Action Update, Fundamenta Informaticae, 44:1-2, (95-131), Online publication date: 1-Jan-2000.
- Mahony B (1999). The Least Conjunctive Refinement and Promotion in the Refinement Calculus, Formal Aspects of Computing, 11:1, (75-105), Online publication date: 1-Sep-1999.
- Gannod G and Cheng B A specification matching based approach to reverse engineering Proceedings of the 21st international conference on Software engineering, (389-398)
- Mallon W, Udding J and Verhoeff T Analysis and Applications of the XDI model Proceedings of the 5th International Symposium on Advanced Research in Asynchronous Circuits and Systems
- Gries D Monotonicity in Calculational Proofs Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the occasion of his retirement from his professorship at the University of Kiel), (79-85)
- Sivilotti P A class of synchronization systems that permit the use of large atomic blocks Proceedings of the 1998 conference of the Centre for Advanced Studies on Collaborative research
- Arora A and Kulkarni S (1998). Designing Masking Fault-Tolerance via Nonmasking Fault-Tolerance, IEEE Transactions on Software Engineering, 24:6, (435-450), Online publication date: 1-Jun-1998.
- Geurts F (1998). Abstract compositional analysis of iterated relations, 10.5555/1743606, Online publication date: 1-Jan-1998.
- Chetali B (1998). Formal Verification of Concurrent Programs Using the Larch Prover, IEEE Transactions on Software Engineering, 24:1, (46-62), Online publication date: 1-Jan-1998.
- Lengauer C, Gorlatch S and Herrmann C (1997). The Static Parallelization of Loops and Recursions, The Journal of Supercomputing, 11:4, (333-353), Online publication date: 1-Dec-1997.
- Bjareland M and Karlsson L Reasoning by regression Proceedings of the Fifteenth international joint conference on Artifical intelligence - Volume 2, (1420-1425)
- Lukaszewicz W and Madalinska-Bugaj E Reasoning about plans Proceedings of the Fifteenth international joint conference on Artifical intelligence - Volume 2, (1215-1220)
- Liu X, Yang H and Zedan H Formal Methods for the Re-Engineering of Computing Systems Proceedings of the 21st International Computer Software and Applications Conference
- Pan S and Dromey R Beyond structured programming Proceedings of the 18th international conference on Software engineering, (268-277)
- Manohar R, Rustan K and Leino M (1995). Conditional composition, Formal Aspects of Computing, 7:6, (683-703), Online publication date: 1-Nov-1995.
- Gorlatch S and Lengauer C (1995). Parallelization of divide-and-conquer in the Bird-Meertens formalism, Formal Aspects of Computing, 7:6, (663-682), Online publication date: 1-Nov-1995.
- Lukaszewicz W and Madaliriska-Bugaj E Reasoning about action and change using Dijkstra's semantics for programming languages Proceedings of the 14th international joint conference on Artificial intelligence - Volume 2, (1950-1955)
- Dromey R (1995). A Model for Software Product Quality, IEEE Transactions on Software Engineering, 21:2, (146-162), Online publication date: 1-Feb-1995.
- van de Snepscheut J (1995). The sliding-window protocol revisited, Formal Aspects of Computing, 7:1, (3-17), Online publication date: 1-Jan-1995.
- Arora A and Gouda M (1993). Closure and Convergence, IEEE Transactions on Software Engineering, 19:11, (1015-1027), Online publication date: 1-Nov-1993.
- Fokkinga M (1992). Calculate categorically!, Formal Aspects of Computing, 4:Suppl 1, (673-692), Online publication date: 1-Nov-1992.
- Lukkien J and van de Snepscheut J (1992). Weakest preconditions for progress, Formal Aspects of Computing, 4:2, (195-236), Online publication date: 1-Mar-1992.
- Broy M Declarative specification and declarative programming Proceedings of the 6th international workshop on Software specification and design, (2-11)
- Ashenhurst R (1991). ACM Forum, Communications of the ACM, 34:9, (16-ff.), Online publication date: 1-Sep-1991.
- Soloway E (1991). How the Nintendo generation learns, Communications of the ACM, 34:9, (23-ff.), Online publication date: 1-Sep-1991.
- Sanders B A predicate transformer approach to knowledge and knowledge-based protocols (extended abstract) Proceedings of the tenth annual ACM symposium on Principles of distributed computing, (217-230)
- Sanders B (1991). Eliminating the substitution axiom from UNITY logic, Formal Aspects of Computing, 3:2, (189-205), Online publication date: 1-Jun-1991.
- Gries D (1991). Teaching calculation and discrimination, Communications of the ACM, 34:3, (44-55), Online publication date: 1-Mar-1991.
- Rao J Reasoning about probabilistic algorithms Proceedings of the ninth annual ACM symposium on Principles of distributed computing, (247-264)
Index Terms
- Predicate calculus and program semantics
Recommendations
A Fixpoint Semantics and an SLD-Resolution Calculus for Modal Logic Programs
We propose a modal logic programming language called MProlog, which is as expressive as the general modal Horn fragment. We give a fixpoint semantics and an SLD-resolution calculus for MProlog in all of the basic serial modal logics KD, T, KDB, B, KD4, ...
A fixpoint semantics and an SLD-resolution calculus for modal logic programs
We propose a modal logic programming language called MProlog, which is as expressive as the general modal Horn fragment. We give a fixpoint semantics and an SLD-resolution calculus for MProlog in all of the basic serial modal logics KD, T, KDB, B, KD4, ...
On Kripke-style Semantics for the Provability Logic of Gödel's Proof Predicate with Quantifiers on Proofs
Kripke-style semantics is suggested for the provability logic with quantifiers on proofs corresponding to the standard Gödel proof predicate. It is proved that the set of valid formulas is decidable. The arithmetical completeness is still an open issue.
...