CN116820564B - Unified form semanticalization method of program language - Google Patents
Unified form semanticalization method of program language Download PDFInfo
- Publication number
- CN116820564B CN116820564B CN202310825407.7A CN202310825407A CN116820564B CN 116820564 B CN116820564 B CN 116820564B CN 202310825407 A CN202310825407 A CN 202310825407A CN 116820564 B CN116820564 B CN 116820564B
- Authority
- CN
- China
- Prior art keywords
- program
- language
- formal
- semantic
- logic structure
- Prior art date
- Legal status (The legal status is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the status listed.)
- Active
Links
- 238000000034 method Methods 0.000 title claims abstract description 46
- 230000006399 behavior Effects 0.000 claims abstract description 12
- 230000008569 process Effects 0.000 claims abstract description 7
- 230000009467 reduction Effects 0.000 claims description 28
- 230000006698 induction Effects 0.000 claims description 20
- 238000012546 transfer Methods 0.000 claims description 17
- 238000004422 calculation algorithm Methods 0.000 claims description 13
- 238000013135 deep learning Methods 0.000 claims description 8
- 230000000694 effects Effects 0.000 claims description 6
- 238000004364 calculation method Methods 0.000 claims description 4
- 230000008859 change Effects 0.000 claims description 3
- 238000011156 evaluation Methods 0.000 claims description 3
- 238000004088 simulation Methods 0.000 claims description 3
- 230000006870 function Effects 0.000 abstract description 3
- 238000012545 processing Methods 0.000 abstract description 3
- 238000005516 engineering process Methods 0.000 abstract description 2
- 238000010276 construction Methods 0.000 abstract 1
- 238000012067 mathematical method Methods 0.000 abstract 1
- 238000013507 mapping Methods 0.000 description 3
- 230000007704 transition Effects 0.000 description 3
- 230000009286 beneficial effect Effects 0.000 description 1
Classifications
-
- Y—GENERAL TAGGING OF NEW TECHNOLOGICAL DEVELOPMENTS; GENERAL TAGGING OF CROSS-SECTIONAL TECHNOLOGIES SPANNING OVER SEVERAL SECTIONS OF THE IPC; TECHNICAL SUBJECTS COVERED BY FORMER USPC CROSS-REFERENCE ART COLLECTIONS [XRACs] AND DIGESTS
- Y02—TECHNOLOGIES OR APPLICATIONS FOR MITIGATION OR ADAPTATION AGAINST CLIMATE CHANGE
- Y02D—CLIMATE CHANGE MITIGATION TECHNOLOGIES IN INFORMATION AND COMMUNICATION TECHNOLOGIES [ICT], I.E. INFORMATION AND COMMUNICATION TECHNOLOGIES AIMING AT THE REDUCTION OF THEIR OWN ENERGY USE
- Y02D10/00—Energy efficient computing, e.g. low power processors, power management or thermal management
Landscapes
- Devices For Executing Special Programs (AREA)
Abstract
The invention relates to a unified form semanteme method of a program language, which belongs to the technical field of electric digital data processing and comprises a generalized mathematical method of program form semanteme, a construction method of form expression semantic operation, a form semantic operation method of an abstract machine and a standardized, structured and formalized method of a thinking type based on a form semantic module generation process. The unified form semanteme method of the program language is not influenced by subjective behaviors of the program language and grammar of different program languages, the characteristics of the program can be extracted, and all functions of the program are reserved, so that experts of non-intelligent technology professionals can understand and analyze the code, and further judge or decide under the corresponding field.
Description
Technical Field
The invention belongs to the technical field of electric digital data processing, and particularly relates to a unified form semanteme method of a program language.
Background
The existing programming languages have higher characteristics, each existing programming language such as C, java, C++, python and the like has grammar characteristics different from other languages, and for a section of known codes, a non-intelligent technical professional expert has difficulty in understanding and analyzing the section of codes and judging or deciding under the corresponding field, and a unified method for uniformly extracting the characteristics of various programming languages does not exist at present.
Therefore, a unified semantic method of a programming language needs to be designed at present to solve the above problems.
Disclosure of Invention
The invention aims to provide a unified form semanteme method of a program language, which is used for solving the technical problems in the prior art, is not influenced by subjective behaviors of the program language and grammar of different programming languages, can refine the characteristics of the program, and retains all functions of the program, so that experts not specialized in intelligent technology can understand and analyze the code, and further judge or decide under the corresponding field.
In order to achieve the above purpose, the technical scheme of the invention is as follows:
a method for unified form semanticalization of a program language, comprising the steps of:
s1, abstracting language components of a program language by using formal semantics; that is, the execution effect of each component in the language is described in an abstract way so as to avoid that the described semantics depend on the specific computer used when the program language is implemented; thereby obtaining a formal language capable of completely describing the programming language;
s2, defining a semantic algorithm of a formal language, and associating a combined logic structure and a reduction relation of a thinking type to enable the program to correspond to the logic structure and the logic structure to correspond to the thinking type;
s3, using a formal language, and defining three types of transfer rules: analyzing, evaluating and executing, wherein grammar of the program language is expressed into abstract form to define algorithm of formal semantic meaning, namely, an abstract machine capable of executing formal language like computer executing program language is constructed;
s4, expanding the logic structure of the program language by using instructions of a program module in deep learning, and semantically obtaining a wider formalized logic structure; thus, the transfer process of the associative combination operation of the logical structure of the program language can be expressed as a reduction relationship between patterns obtained by performing semantic operation on the formalized logical structure through the abstract machine; the formalized logic structure can finally obtain a formal semantic module with larger granularity through formal semantic operation; thus, a correspondence relationship can be established between the formalized logical structure, the thinking type, and the program.
Further, the step S2 specifically includes:
representing the grammar of the program language in abstract form; meanwhile, instructions of the program modules in the deep learning are divided according to the logic structure, and the grammar structure of the basic formal semantic language is expanded.
Further, the step S3 specifically includes:
specifically, the following three types of transfer rules are defined:
simulating thinking logic of a computer running program language, namely analyzing behaviors of the abstract machine;
the simulation computer evaluates the arithmetic expression and the Boolean expression, namely the evaluation behavior of the abstract machine;
simulating the change of the program statement to the state, namely the execution behavior of the abstract machine;
in addition, the state of the computer and the sentence to be executed are formally described by using the patterns, the capability of reducing the complex patterns to be simpler and continuing to maintain the original expression efficacy is called a reduction relation, and the correspondence of the logic structure and the thinking type of the association combination is realized by using the reduction relation.
Further, the step S4 specifically includes:
the method comprises the steps of giving a calculation rule of an expression, a transfer rule of a state and a statement reduction in the form of proposition and theorem; here, not only three operation conditions and conclusions are considered, but also mathematical induction method, structure induction method, yield induction method and rule induction method are utilized to carry out high induction on the operation algorithm of formal semantics, so that the explanation of the unique ending property of the program state operation and the explanation of Church-Rosser property of the maximum state, state accessibility and reachable relation of the transfer relation can be obtained;
after the properties are given, the operation of the program can form the correspondence of the association combination of the program and the logic structure through abstract symbolic language operation, namely formal semantic operation; using a pattern to describe the state of a computer and sentences to be executed, and forming a pattern corresponding to a specific thinking type in a thinking space through a reduction relation of formal semantics;
thus, the association combination of the logic structure and the correspondence of the thinking types can be completed by finding the correspondence of the formal semantic operation and the reduction relationship between the patterns.
Compared with the prior art, the invention has the following beneficial effects:
the method has the advantages that the unified form semantezation method of the program language is not influenced by subjective behaviors of the program language and grammar of different program languages, the characteristics of the program can be extracted, and all functions of the program are reserved, so that experts of non-intelligent technical professionals can understand and analyze the code, and further judge or decide under the corresponding field.
Drawings
Fig. 1 is a schematic flow chart of steps in the embodiment of the present invention.
Detailed Description
For the purpose of making the technical solution and advantages of the present invention more apparent, the present invention will be described in further detail with reference to the accompanying drawings and examples. It should be understood that the particular embodiments described herein are illustrative only and are not intended to limit the invention, i.e., the embodiments described are merely some, but not all, of the embodiments of the invention. The components of the embodiments of the present invention generally described and illustrated in the figures herein may be arranged and designed in a wide variety of different configurations.
Thus, the following detailed description of the embodiments of the invention, as presented in the figures, is not intended to limit the scope of the invention, as claimed, but is merely representative of selected embodiments of the invention. All other embodiments, which can be made by a person skilled in the art without making any inventive effort, are intended to be within the scope of the present invention.
First, language components of a program language need to be abstracted using formal semantics. The basic idea of formal semanteme is to describe the execution effect of each component in the language in an abstract mode, so as to prevent the described semanteme from depending on a specific computer used when the program language is implemented, and enhance the generalization capability of the description language. Meanwhile, instructions of the program modules in the deep learning are divided according to the logic structure, and the grammar structure of the basic formal semantic language is expanded. The effect of doing so is: the transition system based on the structural operation semantics can be universally applied to semantic descriptions of various languages including various distributed languages; our system can be used as its "frame of reference" in analyzing the correctness of other semantics.
Secondly, after the formal semantezation of the program language is completed, a formal language capable of completely describing the program language is obtained. Because of the need to complete the correspondence of the program to the logical structure, the logical structure to the type of thinking, the semantic algorithm of the formal language is defined, as well as the reduction relationship of the logical structure and the type of thinking of the associated combination. The method comprises the steps of expressing grammar of a program language into an abstract form by designing a formal semantic abstract computer, namely an abstract machine for short, so as to obtain an algorithm of formal semantics; the method uses a pattern to formally describe the state of a computer and sentences to be executed, reduces the capability of the pattern of realizing a complex pattern to be simpler and continuously maintaining the original expression effectiveness, namely a reduction relation, and realizes the correspondence of the logic structure and the thinking type of the association combination through the reduction relation.
To better utilize the tightness of mathematical representation, we present the calculation rule of the expression, the transition rule of the state and the way of sentence reduction in the form of proposition and theorem; the three operation conditions, conclusion and proof process are provided, and mathematical induction method, structural induction method, good base induction method and rule induction method are utilized to carry out high induction on the formal semantic operation algorithm, so that the explanation of the unique ending property, the maximum state of transfer relation, the state accessibility and the Church-Rosser property of the reachable relation of program state operation is obtained. Based on the properties, a mapping relation of program operation to a logic structure association combination can be formed, a mapping relation of a pattern to a specific thinking type in the thinking space is formed, and a formalization process and a formalization mode for forming the mapping relation of the types are established.
Finally, we use the reduction relationship of the "AI algorithm form semantic system" to define the understanding module of the program language. In fact, we will prove the transfer of the logical structure and thinking types of the program association combination in the operation process, and can also be expressed as a series of reduction among the patterns, namely, the correspondence of the formal semantic operation and the reduction relationship among the patterns is realized. Thereby realizing the correspondence of the associated combination of the logic structure with the specific thinking type in the thinking space.
Since the transition system based on the structural operation semantics can be universally applied to semantic descriptions of various languages including various distributed languages, and python is one of main stream software for processing deep learning tasks and is similar to other languages, we take python language as an example to describe the above in detail.
As shown in fig. 1, a unified form semanticalization method of a program language is provided, which comprises the following steps:
s1, abstracting language components of a program language by using formal semantics; that is, the execution effect of each component in the language is described in an abstract way so as to avoid that the described semantics depend on the specific computer used when the program language is implemented; thereby obtaining a formal language capable of completely describing the programming language;
s2, defining a semantic algorithm of a formal language, and associating a combined logic structure and a reduction relation of a thinking type to enable the program to correspond to the logic structure and the logic structure to correspond to the thinking type;
s3, using a formal language, and defining three types of transfer rules: analyzing, evaluating and executing, wherein grammar of the program language is expressed into abstract form to define algorithm of formal semantic meaning, namely, an abstract machine capable of executing formal language like computer executing program language is constructed;
s4, expanding the logic structure of the program language by using instructions of a program module in deep learning, and semantically obtaining a wider formalized logic structure; thus, the transfer process of the associative combination operation of the logical structure of the program language can be expressed as a reduction relationship between patterns obtained by performing semantic operation on the formalized logical structure through the abstract machine; the formalized logic structure can finally obtain a formal semantic module with larger granularity through formal semantic operation; thus, a correspondence relationship can be established between the formalized logical structure, the thinking type, and the program.
Further, the step S2 specifically includes:
representing the grammar of the program language in abstract form; meanwhile, instructions of the program modules in the deep learning are divided according to the logic structure, and the grammar structure of the basic formal semantic language is expanded.
Further, the step S3 specifically includes:
specifically, the following three types of transfer rules are defined:
simulating thinking logic of a computer running program language, namely analyzing behaviors of the abstract machine;
the simulation computer evaluates the arithmetic expression and the Boolean expression, namely the evaluation behavior of the abstract machine;
simulating the change of the program statement to the state, namely the execution behavior of the abstract machine;
in addition, the state of the computer and the sentence to be executed are formally described by using the patterns, the capability of reducing the complex patterns to be simpler and continuing to maintain the original expression efficacy is called a reduction relation, and the correspondence of the logic structure and the thinking type of the association combination is realized by using the reduction relation.
Further, the step S4 specifically includes:
the method comprises the steps of giving a calculation rule of an expression, a transfer rule of a state and a statement reduction in the form of proposition and theorem; here, not only three operation conditions and conclusions are considered, but also mathematical induction method, structure induction method, yield induction method and rule induction method are utilized to carry out high induction on the operation algorithm of formal semantics, so that the explanation of the unique ending property of the program state operation and the explanation of Church-Rosser property of the maximum state, state accessibility and reachable relation of the transfer relation can be obtained;
after the properties are given, the operation of the program can form the correspondence of the association combination of the program and the logic structure through abstract symbolic language operation, namely formal semantic operation; using a pattern to describe the state of a computer and sentences to be executed, and forming a pattern corresponding to a specific thinking type in a thinking space through a reduction relation of formal semantics;
thus, the association combination of the logic structure and the correspondence of the thinking types can be completed by finding the correspondence of the formal semantic operation and the reduction relationship between the patterns.
The above is a preferred embodiment of the present invention, and all changes made according to the technical solution of the present invention belong to the protection scope of the present invention when the generated functional effects do not exceed the scope of the technical solution of the present invention.
Claims (4)
1. The unified form semanticalization method of the program language is characterized by comprising the following steps:
s1, abstracting language components of a program language by using formal semantics; that is, the execution effect of each component in the language is described in an abstract way so as to avoid that the described semantics depend on the specific computer used when the program language is implemented; thereby obtaining a formal language capable of completely describing the programming language;
s2, defining a semantic algorithm of a formal language, and associating a combined logic structure and a reduction relation of a thinking type to enable the program to correspond to the logic structure and the logic structure to correspond to the thinking type;
s3, using a formal language, and defining three types of transfer rules: analyzing, evaluating and executing, wherein grammar of the program language is expressed into abstract form to define algorithm of formal semantic meaning, namely, an abstract machine capable of executing formal language like computer executing program language is constructed;
s4, expanding the logic structure of the program language by using instructions of a program module in deep learning, and semantically obtaining a wider formalized logic structure; thus, the transfer process of the associative combination operation of the logical structure of the program language can be expressed as a reduction relationship between patterns obtained by performing semantic operation on the formalized logical structure through the abstract machine; the formalized logic structure can finally obtain a formal semantic module with larger granularity through formal semantic operation; thus, a correspondence relationship can be established between the formalized logical structure, the thinking type, and the program.
2. The method for unified form semanticalization of a program language according to claim 1, wherein the step S2 is specifically as follows:
representing the grammar of the program language in abstract form; meanwhile, instructions of the program modules in the deep learning are divided according to the logic structure, and the grammar structure of the basic formal semantic language is expanded.
3. The method for unified form semanticalization of a program language according to claim 2, wherein the step S3 is specifically as follows:
specifically, the following three types of transfer rules are defined:
simulating thinking logic of a computer running program language, namely analyzing behaviors of the abstract machine;
the simulation computer evaluates the arithmetic expression and the Boolean expression, namely the evaluation behavior of the abstract machine;
simulating the change of the program statement to the state, namely the execution behavior of the abstract machine;
in addition, the state of the computer and the sentence to be executed are formally described by using the patterns, the capability of reducing the complex patterns to be simpler and continuing to maintain the original expression efficacy is called a reduction relation, and the correspondence of the logic structure and the thinking type of the association combination is realized by using the reduction relation.
4. A method of unified semantics of a programming language according to claim 3, wherein step S4 is specifically as follows:
the method comprises the steps of giving a calculation rule of an expression, a transfer rule of a state and a statement reduction in the form of proposition and theorem; here, not only three operation conditions and conclusions are considered, but also mathematical induction method, structural induction method, yield induction method and rule induction method are utilized to carry out high induction on the operation algorithm of formal semantics, so that the explanation of the unique ending property of the program state operation and the explanation of Church-Rosser property of the maximum state, state reachability and reachable relation of the transfer relation can be obtained;
after the properties are given, the operation of the program can form the correspondence of the association combination of the program and the logic structure through abstract symbolic language operation, namely formal semantic operation; using a pattern to describe the state of a computer and sentences to be executed, and forming a pattern corresponding to a specific thinking type in a thinking space through a reduction relation of formal semantics;
thus, the association combination of the logic structure and the correspondence of the thinking types can be completed by finding the correspondence of the formal semantic operation and the reduction relationship between the patterns.
Priority Applications (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| CN202310825407.7A CN116820564B (en) | 2023-07-06 | 2023-07-06 | Unified form semanticalization method of program language |
Applications Claiming Priority (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| CN202310825407.7A CN116820564B (en) | 2023-07-06 | 2023-07-06 | Unified form semanticalization method of program language |
Publications (2)
| Publication Number | Publication Date |
|---|---|
| CN116820564A CN116820564A (en) | 2023-09-29 |
| CN116820564B true CN116820564B (en) | 2024-04-02 |
Family
ID=88139165
Family Applications (1)
| Application Number | Title | Priority Date | Filing Date |
|---|---|---|---|
| CN202310825407.7A Active CN116820564B (en) | 2023-07-06 | 2023-07-06 | Unified form semanticalization method of program language |
Country Status (1)
| Country | Link |
|---|---|
| CN (1) | CN116820564B (en) |
Citations (12)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| US6832365B1 (en) * | 2000-10-11 | 2004-12-14 | Microsoft Corporation | System and method for interacting with computer programming languages at semantic level |
| JP2006085206A (en) * | 2004-09-13 | 2006-03-30 | Kenji Miyamoto | Program base |
| KR20120076810A (en) * | 2010-12-30 | 2012-07-10 | 에스케이 텔레콤주식회사 | Method for extracting semantic information of composite sentence including natural language and mathematical formula, apparatus and computer-readable recording medium with program therefor |
| CN103123590A (en) * | 2011-11-18 | 2013-05-29 | 中国科学院沈阳计算技术研究所有限公司 | Compiling method from intermediate language (IL) program to C language program of instruction list |
| CN103617159A (en) * | 2012-12-07 | 2014-03-05 | 万继华 | Method for translating natural languages into computer language, semantic analyzer and human-machine conversation system |
| US8806453B1 (en) * | 2011-09-15 | 2014-08-12 | Lockheed Martin Corporation | Integrating disparate programming languages to form a new programming language |
| CN112506516A (en) * | 2020-11-30 | 2021-03-16 | 广州市智能软件产业研究院 | Code generation method of security protocol, computer and storage medium |
| CN112835620A (en) * | 2021-02-10 | 2021-05-25 | 中国人民解放军军事科学院国防科技创新研究院 | Semantic similar code online detection method based on deep learning |
| US11100291B1 (en) * | 2015-03-13 | 2021-08-24 | Soundhound, Inc. | Semantic grammar extensibility within a software development framework |
| CN113868136A (en) * | 2021-09-28 | 2021-12-31 | 中南民族大学 | Program vulnerability analysis method based on Go language executable formal semantics |
| CN114138238A (en) * | 2021-11-24 | 2022-03-04 | 中南民族大学 | BPMN2.0 execution engine based on formalized semantics |
| CN114238467A (en) * | 2021-12-01 | 2022-03-25 | 中冶赛迪重庆信息技术有限公司 | Structured data analysis method and system |
Family Cites Families (5)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| US7243086B2 (en) * | 2003-12-19 | 2007-07-10 | Fuji Xerox Co., Ltd. | Methods and systems for automatically generating provably correct computer program code |
| US20050166182A1 (en) * | 2004-01-22 | 2005-07-28 | Microsoft Corporation | Distributed semantic schema |
| US9063744B2 (en) * | 2006-06-26 | 2015-06-23 | Ca, Inc. | Modifying a file written in a formal language |
| EP2454661A1 (en) * | 2009-07-15 | 2012-05-23 | Proviciel - Mlstate | System and method for creating a parser generator and associated computer program |
| US9239710B2 (en) * | 2013-03-15 | 2016-01-19 | ArtinSoft Corporation | Programming language transformations with abstract syntax tree extensions |
-
2023
- 2023-07-06 CN CN202310825407.7A patent/CN116820564B/en active Active
Patent Citations (12)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| US6832365B1 (en) * | 2000-10-11 | 2004-12-14 | Microsoft Corporation | System and method for interacting with computer programming languages at semantic level |
| JP2006085206A (en) * | 2004-09-13 | 2006-03-30 | Kenji Miyamoto | Program base |
| KR20120076810A (en) * | 2010-12-30 | 2012-07-10 | 에스케이 텔레콤주식회사 | Method for extracting semantic information of composite sentence including natural language and mathematical formula, apparatus and computer-readable recording medium with program therefor |
| US8806453B1 (en) * | 2011-09-15 | 2014-08-12 | Lockheed Martin Corporation | Integrating disparate programming languages to form a new programming language |
| CN103123590A (en) * | 2011-11-18 | 2013-05-29 | 中国科学院沈阳计算技术研究所有限公司 | Compiling method from intermediate language (IL) program to C language program of instruction list |
| CN103617159A (en) * | 2012-12-07 | 2014-03-05 | 万继华 | Method for translating natural languages into computer language, semantic analyzer and human-machine conversation system |
| US11100291B1 (en) * | 2015-03-13 | 2021-08-24 | Soundhound, Inc. | Semantic grammar extensibility within a software development framework |
| CN112506516A (en) * | 2020-11-30 | 2021-03-16 | 广州市智能软件产业研究院 | Code generation method of security protocol, computer and storage medium |
| CN112835620A (en) * | 2021-02-10 | 2021-05-25 | 中国人民解放军军事科学院国防科技创新研究院 | Semantic similar code online detection method based on deep learning |
| CN113868136A (en) * | 2021-09-28 | 2021-12-31 | 中南民族大学 | Program vulnerability analysis method based on Go language executable formal semantics |
| CN114138238A (en) * | 2021-11-24 | 2022-03-04 | 中南民族大学 | BPMN2.0 execution engine based on formalized semantics |
| CN114238467A (en) * | 2021-12-01 | 2022-03-25 | 中冶赛迪重庆信息技术有限公司 | Structured data analysis method and system |
Non-Patent Citations (9)
| Title |
|---|
| A structural approach to operational semantics;GORDON D. PLOTKIN;The journal of logic and algebraic programming;全文 * |
| Diletta Romana Cacciagrano * |
| Rosario Culmone.Formal Semantics of an IoT-Specific Language.2018 32nd International Conference on Advanced Information Networking and Applications Workshops (WAINA).2018,全文. * |
| 动态模糊逻辑(DFL)程序设计语言的结构化操作语义;赵小芳;范辉;;计算机应用与软件(第08期);全文 * |
| 形式语义学引论 操作语义学;周巢尘;计算机研究与发展;全文 * |
| 智能神经网络程序设计语言中规则的指称语义;刘晓洁;计算机应用研究;20041231;第21卷(第10期);全文 * |
| 智能神经网络程序设计语言中规则的指称语义;金军, 李涛, 伍良富;四川大学学报(工程科学版);20010328(第02期);全文 * |
| 框架时序逻辑程序语言MSVL的形式语义;杨潇潇;西安电子科技大学 博士学位论文;20091231;全文 * |
| 程序设计语言的形式语义研究进展;计春雷;;上海电机学院学报(第03期);全文 * |
Also Published As
| Publication number | Publication date |
|---|---|
| CN116820564A (en) | 2023-09-29 |
Similar Documents
| Publication | Publication Date | Title |
|---|---|---|
| Visser et al. | Building program optimizers with rewriting strategies | |
| Afshari et al. | Cut-free completeness for modal mu-calculus | |
| Chockler et al. | Incremental formal verification of hardware | |
| D’Agostino et al. | Semantics and proof-theory of depth bounded Boolean logics | |
| CN113987405A (en) | AST-based mathematical expression calculation algorithm | |
| Zhao et al. | Program behavior discovery and verification: A graph grammar approach | |
| Gurevich | Foundational analyses of computation | |
| CN116820564B (en) | Unified form semanticalization method of program language | |
| Gorlin et al. | Model checking with probabilistic tabled logic programming | |
| Bogaerts et al. | Declarative solver development: Case studies | |
| Farheen | Improvements to transitive-closure-based model checking in Alloy | |
| Percebois et al. | Rule-level verification of graph transformations for invariants based on edges’ transitive closure | |
| CN111679809B (en) | Program development and verification method and system based on Noesis logic | |
| Köhl | An executable structural operational formal semantics for Python | |
| CN113835688B (en) | Object packaging method of scientific computing language interpreter | |
| Kieburtz | P-logic: Property verification for Haskell programs | |
| Gaintzarain et al. | Systematic semantic tableaux for PLTL | |
| Bensalem et al. | Abstraction as the key for invariant verification | |
| Bodeveix et al. | Experimenting Acceleration Methods for the Validation of Infinite State Systems. | |
| Ehm | The Kleene algebra of nested pointer structures: theory and applications. | |
| Rafe et al. | ASM2Bogor: An approach for verification of models specified through Asmeta language | |
| Lange et al. | Capturing bisimulation-invariant complexity classes with higher-order modal fixpoint logic | |
| Ray et al. | The Complexity of Optimal Planning and a More Efficient Method for Finding Solutions. | |
| Kroening et al. | Second-order SAT solving using program synthesis | |
| Fang et al. | Generalized Strategy Synthesis of Infinite-state Impartial Combinatorial Games via Exact Binary Classification |
Legal Events
| Date | Code | Title | Description |
|---|---|---|---|
| PB01 | Publication | ||
| PB01 | Publication | ||
| SE01 | Entry into force of request for substantive examination | ||
| SE01 | Entry into force of request for substantive examination | ||
| GR01 | Patent grant | ||
| GR01 | Patent grant |