Formal verification of Matrix based MATLAB models using interactive theorem proving Article Swipe
Ayesha Gauhar
,
Adnan Rashid
,
Osman Hasan
,
João Bispo
,
João M. P. Cardoso
·
YOU?
·
· 2021
· Open Access
·
· DOI: https://doi.org/10.7717/peerj-cs.440
YOU?
·
· 2021
· Open Access
·
· DOI: https://doi.org/10.7717/peerj-cs.440
MATLAB is a software based analysis environment that supports a high-level programing language and is widely used to model and analyze systems in various domains of engineering and sciences. Traditionally, the analysis of MATLAB models is done using simulation and debugging/testing frameworks. These methods provide limited coverage due to their inherent incompleteness. Formal verification can overcome these limitations, but developing the formal models of the underlying MATLAB models is a very challenging and time-consuming task, especially in the case of higher-order-logic models. To facilitate this process, we present a library of higher-order-logic functions corresponding to the commonly used matrix functions of MATLAB as well as a translator that allows automatic conversion of MATLAB models to higher-order logic. The formal models can then be formally verified in an interactive theorem prover. For illustrating the usefulness of the proposed library and approach, we present the formal analysis of a Finite Impulse Response (FIR) filter, which is quite commonly used in digital signal processing applications, within the sound core of the HOL Light theorem prover.
Related Topics
Concepts
Metadata
- Type
- article
- Language
- en
- Landing Page
- https://doi.org/10.7717/peerj-cs.440
- OA Status
- gold
- Cited By
- 5
- References
- 39
- Related Works
- 10
- OpenAlex ID
- https://openalex.org/W3137335834
All OpenAlex metadata
Raw OpenAlex JSON
- OpenAlex ID
-
https://openalex.org/W3137335834Canonical identifier for this work in OpenAlex
- DOI
-
https://doi.org/10.7717/peerj-cs.440Digital Object Identifier
- Title
-
Formal verification of Matrix based MATLAB models using interactive theorem provingWork title
- Type
-
articleOpenAlex work type
- Language
-
enPrimary language
- Publication year
-
2021Year of publication
- Publication date
-
2021-03-22Full publication date if available
- Authors
-
Ayesha Gauhar, Adnan Rashid, Osman Hasan, João Bispo, João M. P. CardosoList of authors in order
- Landing page
-
https://doi.org/10.7717/peerj-cs.440Publisher landing page
- Open access
-
YesWhether a free full text is available
- OA status
-
goldOpen access status per OpenAlex
- OA URL
-
https://doi.org/10.7717/peerj-cs.440Direct OA link when available
- Concepts
-
MATLAB, Computer science, Automated theorem proving, HOL, Programming language, Debugging, Formal methods, Formal verification, Gas meter prover, Proof assistant, Process (computing), Theoretical computer science, Algorithm, Computational science, Mathematical proof, Mathematics, GeometryTop concepts (fields/topics) attached by OpenAlex
- Cited by
-
5Total citation count in OpenAlex
- Citations by year (recent)
-
2025: 1, 2023: 2, 2021: 2Per-year citation counts (last 5 years)
- References (count)
-
39Number of works referenced by this work
- Related works (count)
-
10Other works algorithmically related by OpenAlex
Full payload
| id | https://openalex.org/W3137335834 |
|---|---|
| doi | https://doi.org/10.7717/peerj-cs.440 |
| ids.doi | https://doi.org/10.7717/peerj-cs.440 |
| ids.mag | 3137335834 |
| ids.openalex | https://openalex.org/W3137335834 |
| fwci | 1.02259533 |
| type | article |
| title | Formal verification of Matrix based MATLAB models using interactive theorem proving |
| biblio.issue | |
| biblio.volume | 7 |
| biblio.last_page | e440 |
| biblio.first_page | e440 |
| topics[0].id | https://openalex.org/T10904 |
| topics[0].field.id | https://openalex.org/fields/17 |
| topics[0].field.display_name | Computer Science |
| topics[0].score | 0.9990000128746033 |
| topics[0].domain.id | https://openalex.org/domains/3 |
| topics[0].domain.display_name | Physical Sciences |
| topics[0].subfield.id | https://openalex.org/subfields/1708 |
| topics[0].subfield.display_name | Hardware and Architecture |
| topics[0].display_name | Embedded Systems Design Techniques |
| topics[1].id | https://openalex.org/T10142 |
| topics[1].field.id | https://openalex.org/fields/17 |
| topics[1].field.display_name | Computer Science |
| topics[1].score | 0.9987000226974487 |
| topics[1].domain.id | https://openalex.org/domains/3 |
| topics[1].domain.display_name | Physical Sciences |
| topics[1].subfield.id | https://openalex.org/subfields/1703 |
| topics[1].subfield.display_name | Computational Theory and Mathematics |
| topics[1].display_name | Formal Methods in Verification |
| topics[2].id | https://openalex.org/T10126 |
| topics[2].field.id | https://openalex.org/fields/17 |
| topics[2].field.display_name | Computer Science |
| topics[2].score | 0.994700014591217 |
| topics[2].domain.id | https://openalex.org/domains/3 |
| topics[2].domain.display_name | Physical Sciences |
| topics[2].subfield.id | https://openalex.org/subfields/1702 |
| topics[2].subfield.display_name | Artificial Intelligence |
| topics[2].display_name | Logic, programming, and type systems |
| is_xpac | False |
| apc_list.value | 1395 |
| apc_list.currency | USD |
| apc_list.value_usd | 1395 |
| apc_paid.value | 1395 |
| apc_paid.currency | USD |
| apc_paid.value_usd | 1395 |
| concepts[0].id | https://openalex.org/C2780365114 |
| concepts[0].level | 2 |
| concepts[0].score | 0.7596632242202759 |
| concepts[0].wikidata | https://www.wikidata.org/wiki/Q169478 |
| concepts[0].display_name | MATLAB |
| concepts[1].id | https://openalex.org/C41008148 |
| concepts[1].level | 0 |
| concepts[1].score | 0.7565692663192749 |
| concepts[1].wikidata | https://www.wikidata.org/wiki/Q21198 |
| concepts[1].display_name | Computer science |
| concepts[2].id | https://openalex.org/C206880738 |
| concepts[2].level | 2 |
| concepts[2].score | 0.7271277904510498 |
| concepts[2].wikidata | https://www.wikidata.org/wiki/Q431667 |
| concepts[2].display_name | Automated theorem proving |
| concepts[3].id | https://openalex.org/C17435882 |
| concepts[3].level | 2 |
| concepts[3].score | 0.6179918646812439 |
| concepts[3].wikidata | https://www.wikidata.org/wiki/Q17030435 |
| concepts[3].display_name | HOL |
| concepts[4].id | https://openalex.org/C199360897 |
| concepts[4].level | 1 |
| concepts[4].score | 0.5797603726387024 |
| concepts[4].wikidata | https://www.wikidata.org/wiki/Q9143 |
| concepts[4].display_name | Programming language |
| concepts[5].id | https://openalex.org/C168065819 |
| concepts[5].level | 2 |
| concepts[5].score | 0.565604567527771 |
| concepts[5].wikidata | https://www.wikidata.org/wiki/Q845566 |
| concepts[5].display_name | Debugging |
| concepts[6].id | https://openalex.org/C75606506 |
| concepts[6].level | 2 |
| concepts[6].score | 0.4863734543323517 |
| concepts[6].wikidata | https://www.wikidata.org/wiki/Q1049183 |
| concepts[6].display_name | Formal methods |
| concepts[7].id | https://openalex.org/C111498074 |
| concepts[7].level | 2 |
| concepts[7].score | 0.4804075062274933 |
| concepts[7].wikidata | https://www.wikidata.org/wiki/Q173326 |
| concepts[7].display_name | Formal verification |
| concepts[8].id | https://openalex.org/C159718280 |
| concepts[8].level | 3 |
| concepts[8].score | 0.43269675970077515 |
| concepts[8].wikidata | https://www.wikidata.org/wiki/Q5526353 |
| concepts[8].display_name | Gas meter prover |
| concepts[9].id | https://openalex.org/C203265346 |
| concepts[9].level | 3 |
| concepts[9].score | 0.4229433238506317 |
| concepts[9].wikidata | https://www.wikidata.org/wiki/Q11387554 |
| concepts[9].display_name | Proof assistant |
| concepts[10].id | https://openalex.org/C98045186 |
| concepts[10].level | 2 |
| concepts[10].score | 0.4188540577888489 |
| concepts[10].wikidata | https://www.wikidata.org/wiki/Q205663 |
| concepts[10].display_name | Process (computing) |
| concepts[11].id | https://openalex.org/C80444323 |
| concepts[11].level | 1 |
| concepts[11].score | 0.4022318124771118 |
| concepts[11].wikidata | https://www.wikidata.org/wiki/Q2878974 |
| concepts[11].display_name | Theoretical computer science |
| concepts[12].id | https://openalex.org/C11413529 |
| concepts[12].level | 1 |
| concepts[12].score | 0.3767140507698059 |
| concepts[12].wikidata | https://www.wikidata.org/wiki/Q8366 |
| concepts[12].display_name | Algorithm |
| concepts[13].id | https://openalex.org/C459310 |
| concepts[13].level | 1 |
| concepts[13].score | 0.3714870512485504 |
| concepts[13].wikidata | https://www.wikidata.org/wiki/Q117801 |
| concepts[13].display_name | Computational science |
| concepts[14].id | https://openalex.org/C108710211 |
| concepts[14].level | 2 |
| concepts[14].score | 0.2548167109489441 |
| concepts[14].wikidata | https://www.wikidata.org/wiki/Q11538 |
| concepts[14].display_name | Mathematical proof |
| concepts[15].id | https://openalex.org/C33923547 |
| concepts[15].level | 0 |
| concepts[15].score | 0.1567366123199463 |
| concepts[15].wikidata | https://www.wikidata.org/wiki/Q395 |
| concepts[15].display_name | Mathematics |
| concepts[16].id | https://openalex.org/C2524010 |
| concepts[16].level | 1 |
| concepts[16].score | 0.0 |
| concepts[16].wikidata | https://www.wikidata.org/wiki/Q8087 |
| concepts[16].display_name | Geometry |
| keywords[0].id | https://openalex.org/keywords/matlab |
| keywords[0].score | 0.7596632242202759 |
| keywords[0].display_name | MATLAB |
| keywords[1].id | https://openalex.org/keywords/computer-science |
| keywords[1].score | 0.7565692663192749 |
| keywords[1].display_name | Computer science |
| keywords[2].id | https://openalex.org/keywords/automated-theorem-proving |
| keywords[2].score | 0.7271277904510498 |
| keywords[2].display_name | Automated theorem proving |
| keywords[3].id | https://openalex.org/keywords/hol |
| keywords[3].score | 0.6179918646812439 |
| keywords[3].display_name | HOL |
| keywords[4].id | https://openalex.org/keywords/programming-language |
| keywords[4].score | 0.5797603726387024 |
| keywords[4].display_name | Programming language |
| keywords[5].id | https://openalex.org/keywords/debugging |
| keywords[5].score | 0.565604567527771 |
| keywords[5].display_name | Debugging |
| keywords[6].id | https://openalex.org/keywords/formal-methods |
| keywords[6].score | 0.4863734543323517 |
| keywords[6].display_name | Formal methods |
| keywords[7].id | https://openalex.org/keywords/formal-verification |
| keywords[7].score | 0.4804075062274933 |
| keywords[7].display_name | Formal verification |
| keywords[8].id | https://openalex.org/keywords/gas-meter-prover |
| keywords[8].score | 0.43269675970077515 |
| keywords[8].display_name | Gas meter prover |
| keywords[9].id | https://openalex.org/keywords/proof-assistant |
| keywords[9].score | 0.4229433238506317 |
| keywords[9].display_name | Proof assistant |
| keywords[10].id | https://openalex.org/keywords/process |
| keywords[10].score | 0.4188540577888489 |
| keywords[10].display_name | Process (computing) |
| keywords[11].id | https://openalex.org/keywords/theoretical-computer-science |
| keywords[11].score | 0.4022318124771118 |
| keywords[11].display_name | Theoretical computer science |
| keywords[12].id | https://openalex.org/keywords/algorithm |
| keywords[12].score | 0.3767140507698059 |
| keywords[12].display_name | Algorithm |
| keywords[13].id | https://openalex.org/keywords/computational-science |
| keywords[13].score | 0.3714870512485504 |
| keywords[13].display_name | Computational science |
| keywords[14].id | https://openalex.org/keywords/mathematical-proof |
| keywords[14].score | 0.2548167109489441 |
| keywords[14].display_name | Mathematical proof |
| keywords[15].id | https://openalex.org/keywords/mathematics |
| keywords[15].score | 0.1567366123199463 |
| keywords[15].display_name | Mathematics |
| language | en |
| locations[0].id | doi:10.7717/peerj-cs.440 |
| locations[0].is_oa | True |
| locations[0].source.id | https://openalex.org/S4210178049 |
| locations[0].source.issn | 2376-5992 |
| locations[0].source.type | journal |
| locations[0].source.is_oa | True |
| locations[0].source.issn_l | 2376-5992 |
| locations[0].source.is_core | True |
| locations[0].source.is_in_doaj | True |
| locations[0].source.display_name | PeerJ Computer Science |
| locations[0].source.host_organization | https://openalex.org/P4310320104 |
| locations[0].source.host_organization_name | PeerJ, Inc. |
| locations[0].source.host_organization_lineage | https://openalex.org/P4310320104 |
| locations[0].source.host_organization_lineage_names | PeerJ, Inc. |
| locations[0].license | cc-by |
| locations[0].pdf_url | |
| locations[0].version | publishedVersion |
| locations[0].raw_type | journal-article |
| locations[0].license_id | https://openalex.org/licenses/cc-by |
| locations[0].is_accepted | True |
| locations[0].is_published | True |
| locations[0].raw_source_name | PeerJ Computer Science |
| locations[0].landing_page_url | https://doi.org/10.7717/peerj-cs.440 |
| locations[1].id | pmh:oai:doaj.org/article:6d6999bea0104f85bbbff75e19aaf02c |
| locations[1].is_oa | True |
| locations[1].source.id | https://openalex.org/S4306401280 |
| locations[1].source.issn | |
| locations[1].source.type | repository |
| locations[1].source.is_oa | False |
| locations[1].source.issn_l | |
| locations[1].source.is_core | False |
| locations[1].source.is_in_doaj | False |
| locations[1].source.display_name | DOAJ (DOAJ: Directory of Open Access Journals) |
| locations[1].source.host_organization | |
| locations[1].source.host_organization_name | |
| locations[1].license | cc-by-sa |
| locations[1].pdf_url | |
| locations[1].version | submittedVersion |
| locations[1].raw_type | article |
| locations[1].license_id | https://openalex.org/licenses/cc-by-sa |
| locations[1].is_accepted | False |
| locations[1].is_published | False |
| locations[1].raw_source_name | PeerJ Computer Science, Vol 7, p e440 (2021) |
| locations[1].landing_page_url | https://doaj.org/article/6d6999bea0104f85bbbff75e19aaf02c |
| locations[2].id | pmh:oai:pubmedcentral.nih.gov:8022509 |
| locations[2].is_oa | True |
| locations[2].source.id | https://openalex.org/S2764455111 |
| locations[2].source.issn | |
| locations[2].source.type | repository |
| locations[2].source.is_oa | False |
| locations[2].source.issn_l | |
| locations[2].source.is_core | False |
| locations[2].source.is_in_doaj | False |
| locations[2].source.display_name | PubMed Central |
| locations[2].source.host_organization | https://openalex.org/I1299303238 |
| locations[2].source.host_organization_name | National Institutes of Health |
| locations[2].source.host_organization_lineage | https://openalex.org/I1299303238 |
| locations[2].license | cc-by |
| locations[2].pdf_url | |
| locations[2].version | submittedVersion |
| locations[2].raw_type | Text |
| locations[2].license_id | https://openalex.org/licenses/cc-by |
| locations[2].is_accepted | False |
| locations[2].is_published | False |
| locations[2].raw_source_name | PeerJ Comput Sci |
| locations[2].landing_page_url | https://www.ncbi.nlm.nih.gov/pmc/articles/8022509 |
| indexed_in | crossref, doaj |
| authorships[0].author.id | https://openalex.org/A5073216531 |
| authorships[0].author.orcid | |
| authorships[0].author.display_name | Ayesha Gauhar |
| authorships[0].countries | PK |
| authorships[0].affiliations[0].institution_ids | https://openalex.org/I929597975 |
| authorships[0].affiliations[0].raw_affiliation_string | School of Electrical Engineering and Computer Science (SEECS), National University of Sciences and Technology (NUST), Islamabad, Pakistan |
| authorships[0].institutions[0].id | https://openalex.org/I929597975 |
| authorships[0].institutions[0].ror | https://ror.org/03w2j5y17 |
| authorships[0].institutions[0].type | education |
| authorships[0].institutions[0].lineage | https://openalex.org/I929597975 |
| authorships[0].institutions[0].country_code | PK |
| authorships[0].institutions[0].display_name | National University of Sciences and Technology |
| authorships[0].author_position | first |
| authorships[0].raw_author_name | Ayesha Gauhar |
| authorships[0].is_corresponding | False |
| authorships[0].raw_affiliation_strings | School of Electrical Engineering and Computer Science (SEECS), National University of Sciences and Technology (NUST), Islamabad, Pakistan |
| authorships[1].author.id | https://openalex.org/A5015888124 |
| authorships[1].author.orcid | https://orcid.org/0000-0002-9729-584X |
| authorships[1].author.display_name | Adnan Rashid |
| authorships[1].countries | PK |
| authorships[1].affiliations[0].institution_ids | https://openalex.org/I929597975 |
| authorships[1].affiliations[0].raw_affiliation_string | School of Electrical Engineering and Computer Science (SEECS), National University of Sciences and Technology (NUST), Islamabad, Pakistan |
| authorships[1].institutions[0].id | https://openalex.org/I929597975 |
| authorships[1].institutions[0].ror | https://ror.org/03w2j5y17 |
| authorships[1].institutions[0].type | education |
| authorships[1].institutions[0].lineage | https://openalex.org/I929597975 |
| authorships[1].institutions[0].country_code | PK |
| authorships[1].institutions[0].display_name | National University of Sciences and Technology |
| authorships[1].author_position | middle |
| authorships[1].raw_author_name | Adnan Rashid |
| authorships[1].is_corresponding | False |
| authorships[1].raw_affiliation_strings | School of Electrical Engineering and Computer Science (SEECS), National University of Sciences and Technology (NUST), Islamabad, Pakistan |
| authorships[2].author.id | https://openalex.org/A5066768973 |
| authorships[2].author.orcid | https://orcid.org/0000-0003-2562-2669 |
| authorships[2].author.display_name | Osman Hasan |
| authorships[2].countries | PK |
| authorships[2].affiliations[0].institution_ids | https://openalex.org/I929597975 |
| authorships[2].affiliations[0].raw_affiliation_string | School of Electrical Engineering and Computer Science (SEECS), National University of Sciences and Technology (NUST), Islamabad, Pakistan |
| authorships[2].institutions[0].id | https://openalex.org/I929597975 |
| authorships[2].institutions[0].ror | https://ror.org/03w2j5y17 |
| authorships[2].institutions[0].type | education |
| authorships[2].institutions[0].lineage | https://openalex.org/I929597975 |
| authorships[2].institutions[0].country_code | PK |
| authorships[2].institutions[0].display_name | National University of Sciences and Technology |
| authorships[2].author_position | middle |
| authorships[2].raw_author_name | Osman Hasan |
| authorships[2].is_corresponding | False |
| authorships[2].raw_affiliation_strings | School of Electrical Engineering and Computer Science (SEECS), National University of Sciences and Technology (NUST), Islamabad, Pakistan |
| authorships[3].author.id | https://openalex.org/A5028954771 |
| authorships[3].author.orcid | https://orcid.org/0000-0002-3017-9449 |
| authorships[3].author.display_name | João Bispo |
| authorships[3].countries | PT |
| authorships[3].affiliations[0].institution_ids | https://openalex.org/I182534213 |
| authorships[3].affiliations[0].raw_affiliation_string | Faculty of Engineering, University of Porto, Porto, Portugal |
| authorships[3].institutions[0].id | https://openalex.org/I182534213 |
| authorships[3].institutions[0].ror | https://ror.org/043pwc612 |
| authorships[3].institutions[0].type | education |
| authorships[3].institutions[0].lineage | https://openalex.org/I182534213 |
| authorships[3].institutions[0].country_code | PT |
| authorships[3].institutions[0].display_name | Universidade do Porto |
| authorships[3].author_position | middle |
| authorships[3].raw_author_name | João Bispo |
| authorships[3].is_corresponding | False |
| authorships[3].raw_affiliation_strings | Faculty of Engineering, University of Porto, Porto, Portugal |
| authorships[4].author.id | https://openalex.org/A5007667456 |
| authorships[4].author.orcid | https://orcid.org/0000-0002-7353-1799 |
| authorships[4].author.display_name | João M. P. Cardoso |
| authorships[4].countries | PT |
| authorships[4].affiliations[0].institution_ids | https://openalex.org/I182534213 |
| authorships[4].affiliations[0].raw_affiliation_string | Faculty of Engineering, University of Porto, Porto, Portugal |
| authorships[4].institutions[0].id | https://openalex.org/I182534213 |
| authorships[4].institutions[0].ror | https://ror.org/043pwc612 |
| authorships[4].institutions[0].type | education |
| authorships[4].institutions[0].lineage | https://openalex.org/I182534213 |
| authorships[4].institutions[0].country_code | PT |
| authorships[4].institutions[0].display_name | Universidade do Porto |
| authorships[4].author_position | last |
| authorships[4].raw_author_name | João M.P. Cardoso |
| authorships[4].is_corresponding | False |
| authorships[4].raw_affiliation_strings | Faculty of Engineering, University of Porto, Porto, Portugal |
| has_content.pdf | False |
| has_content.grobid_xml | False |
| is_paratext | False |
| open_access.is_oa | True |
| open_access.oa_url | https://doi.org/10.7717/peerj-cs.440 |
| open_access.oa_status | gold |
| open_access.any_repository_has_fulltext | False |
| created_date | 2025-10-10T00:00:00 |
| display_name | Formal verification of Matrix based MATLAB models using interactive theorem proving |
| has_fulltext | False |
| is_retracted | False |
| updated_date | 2025-11-06T03:46:38.306776 |
| primary_topic.id | https://openalex.org/T10904 |
| primary_topic.field.id | https://openalex.org/fields/17 |
| primary_topic.field.display_name | Computer Science |
| primary_topic.score | 0.9990000128746033 |
| primary_topic.domain.id | https://openalex.org/domains/3 |
| primary_topic.domain.display_name | Physical Sciences |
| primary_topic.subfield.id | https://openalex.org/subfields/1708 |
| primary_topic.subfield.display_name | Hardware and Architecture |
| primary_topic.display_name | Embedded Systems Design Techniques |
| related_works | https://openalex.org/W2888810578, https://openalex.org/W4289666903, https://openalex.org/W2769609281, https://openalex.org/W2483392883, https://openalex.org/W2534028225, https://openalex.org/W2809689211, https://openalex.org/W2519051298, https://openalex.org/W4293192252, https://openalex.org/W1504680642, https://openalex.org/W1909465604 |
| cited_by_count | 5 |
| counts_by_year[0].year | 2025 |
| counts_by_year[0].cited_by_count | 1 |
| counts_by_year[1].year | 2023 |
| counts_by_year[1].cited_by_count | 2 |
| counts_by_year[2].year | 2021 |
| counts_by_year[2].cited_by_count | 2 |
| locations_count | 3 |
| best_oa_location.id | doi:10.7717/peerj-cs.440 |
| best_oa_location.is_oa | True |
| best_oa_location.source.id | https://openalex.org/S4210178049 |
| best_oa_location.source.issn | 2376-5992 |
| best_oa_location.source.type | journal |
| best_oa_location.source.is_oa | True |
| best_oa_location.source.issn_l | 2376-5992 |
| best_oa_location.source.is_core | True |
| best_oa_location.source.is_in_doaj | True |
| best_oa_location.source.display_name | PeerJ Computer Science |
| best_oa_location.source.host_organization | https://openalex.org/P4310320104 |
| best_oa_location.source.host_organization_name | PeerJ, Inc. |
| best_oa_location.source.host_organization_lineage | https://openalex.org/P4310320104 |
| best_oa_location.source.host_organization_lineage_names | PeerJ, Inc. |
| best_oa_location.license | cc-by |
| best_oa_location.pdf_url | |
| best_oa_location.version | publishedVersion |
| best_oa_location.raw_type | journal-article |
| best_oa_location.license_id | https://openalex.org/licenses/cc-by |
| best_oa_location.is_accepted | True |
| best_oa_location.is_published | True |
| best_oa_location.raw_source_name | PeerJ Computer Science |
| best_oa_location.landing_page_url | https://doi.org/10.7717/peerj-cs.440 |
| primary_location.id | doi:10.7717/peerj-cs.440 |
| primary_location.is_oa | True |
| primary_location.source.id | https://openalex.org/S4210178049 |
| primary_location.source.issn | 2376-5992 |
| primary_location.source.type | journal |
| primary_location.source.is_oa | True |
| primary_location.source.issn_l | 2376-5992 |
| primary_location.source.is_core | True |
| primary_location.source.is_in_doaj | True |
| primary_location.source.display_name | PeerJ Computer Science |
| primary_location.source.host_organization | https://openalex.org/P4310320104 |
| primary_location.source.host_organization_name | PeerJ, Inc. |
| primary_location.source.host_organization_lineage | https://openalex.org/P4310320104 |
| primary_location.source.host_organization_lineage_names | PeerJ, Inc. |
| primary_location.license | cc-by |
| primary_location.pdf_url | |
| primary_location.version | publishedVersion |
| primary_location.raw_type | journal-article |
| primary_location.license_id | https://openalex.org/licenses/cc-by |
| primary_location.is_accepted | True |
| primary_location.is_published | True |
| primary_location.raw_source_name | PeerJ Computer Science |
| primary_location.landing_page_url | https://doi.org/10.7717/peerj-cs.440 |
| publication_date | 2021-03-22 |
| publication_year | 2021 |
| referenced_works | https://openalex.org/W81013672, https://openalex.org/W6623758801, https://openalex.org/W2770430340, https://openalex.org/W1975906542, https://openalex.org/W147593471, https://openalex.org/W2099661188, https://openalex.org/W3137335834, https://openalex.org/W1545409775, https://openalex.org/W1600435877, https://openalex.org/W2091456056, https://openalex.org/W6724702088, https://openalex.org/W6695206274, https://openalex.org/W1802815921, https://openalex.org/W6604229463, https://openalex.org/W6689083012, https://openalex.org/W6713582119, https://openalex.org/W6631954194, https://openalex.org/W2618528743, https://openalex.org/W39058212, https://openalex.org/W1580053281, https://openalex.org/W2894133236, https://openalex.org/W3048394024, https://openalex.org/W2096231567, https://openalex.org/W1955580075, https://openalex.org/W2162843658, https://openalex.org/W2277766137, https://openalex.org/W4285719527, https://openalex.org/W855611208, https://openalex.org/W1597236814, https://openalex.org/W4229897592, https://openalex.org/W1506809288, https://openalex.org/W102077139, https://openalex.org/W1601195943, https://openalex.org/W2964145825, https://openalex.org/W2229094708, https://openalex.org/W1486242743, https://openalex.org/W2799968324, https://openalex.org/W2500782055, https://openalex.org/W2406128552 |
| referenced_works_count | 39 |
| abstract_inverted_index.a | 2, 9, 69, 88, 105, 146 |
| abstract_inverted_index.To | 82 |
| abstract_inverted_index.an | 126 |
| abstract_inverted_index.as | 102, 104 |
| abstract_inverted_index.be | 122 |
| abstract_inverted_index.in | 22, 76, 125, 157 |
| abstract_inverted_index.is | 1, 14, 35, 68, 153 |
| abstract_inverted_index.of | 25, 32, 63, 79, 90, 100, 111, 134, 145, 166 |
| abstract_inverted_index.to | 17, 48, 94, 114 |
| abstract_inverted_index.we | 86, 140 |
| abstract_inverted_index.For | 130 |
| abstract_inverted_index.HOL | 168 |
| abstract_inverted_index.The | 117 |
| abstract_inverted_index.and | 13, 19, 27, 39, 72, 138 |
| abstract_inverted_index.but | 58 |
| abstract_inverted_index.can | 54, 120 |
| abstract_inverted_index.due | 47 |
| abstract_inverted_index.the | 30, 60, 64, 77, 95, 132, 135, 142, 163, 167 |
| abstract_inverted_index.case | 78 |
| abstract_inverted_index.core | 165 |
| abstract_inverted_index.done | 36 |
| abstract_inverted_index.that | 7, 107 |
| abstract_inverted_index.then | 121 |
| abstract_inverted_index.this | 84 |
| abstract_inverted_index.used | 16, 97, 156 |
| abstract_inverted_index.very | 70 |
| abstract_inverted_index.well | 103 |
| abstract_inverted_index.(FIR) | 150 |
| abstract_inverted_index.Light | 169 |
| abstract_inverted_index.These | 42 |
| abstract_inverted_index.based | 4 |
| abstract_inverted_index.model | 18 |
| abstract_inverted_index.quite | 154 |
| abstract_inverted_index.sound | 164 |
| abstract_inverted_index.task, | 74 |
| abstract_inverted_index.their | 49 |
| abstract_inverted_index.these | 56 |
| abstract_inverted_index.using | 37 |
| abstract_inverted_index.which | 152 |
| abstract_inverted_index.Finite | 147 |
| abstract_inverted_index.Formal | 52 |
| abstract_inverted_index.MATLAB | 0, 33, 66, 101, 112 |
| abstract_inverted_index.allows | 108 |
| abstract_inverted_index.formal | 61, 118, 143 |
| abstract_inverted_index.logic. | 116 |
| abstract_inverted_index.matrix | 98 |
| abstract_inverted_index.models | 34, 62, 67, 113, 119 |
| abstract_inverted_index.signal | 159 |
| abstract_inverted_index.widely | 15 |
| abstract_inverted_index.within | 162 |
| abstract_inverted_index.Impulse | 148 |
| abstract_inverted_index.analyze | 20 |
| abstract_inverted_index.digital | 158 |
| abstract_inverted_index.domains | 24 |
| abstract_inverted_index.filter, | 151 |
| abstract_inverted_index.library | 89, 137 |
| abstract_inverted_index.limited | 45 |
| abstract_inverted_index.methods | 43 |
| abstract_inverted_index.models. | 81 |
| abstract_inverted_index.present | 87, 141 |
| abstract_inverted_index.prover. | 129, 171 |
| abstract_inverted_index.provide | 44 |
| abstract_inverted_index.systems | 21 |
| abstract_inverted_index.theorem | 128, 170 |
| abstract_inverted_index.various | 23 |
| abstract_inverted_index.Response | 149 |
| abstract_inverted_index.analysis | 5, 31, 144 |
| abstract_inverted_index.commonly | 96, 155 |
| abstract_inverted_index.coverage | 46 |
| abstract_inverted_index.formally | 123 |
| abstract_inverted_index.inherent | 50 |
| abstract_inverted_index.language | 12 |
| abstract_inverted_index.overcome | 55 |
| abstract_inverted_index.process, | 85 |
| abstract_inverted_index.proposed | 136 |
| abstract_inverted_index.software | 3 |
| abstract_inverted_index.supports | 8 |
| abstract_inverted_index.verified | 124 |
| abstract_inverted_index.approach, | 139 |
| abstract_inverted_index.automatic | 109 |
| abstract_inverted_index.functions | 92, 99 |
| abstract_inverted_index.sciences. | 28 |
| abstract_inverted_index.conversion | 110 |
| abstract_inverted_index.developing | 59 |
| abstract_inverted_index.especially | 75 |
| abstract_inverted_index.facilitate | 83 |
| abstract_inverted_index.high-level | 10 |
| abstract_inverted_index.processing | 160 |
| abstract_inverted_index.programing | 11 |
| abstract_inverted_index.simulation | 38 |
| abstract_inverted_index.translator | 106 |
| abstract_inverted_index.underlying | 65 |
| abstract_inverted_index.usefulness | 133 |
| abstract_inverted_index.challenging | 71 |
| abstract_inverted_index.engineering | 26 |
| abstract_inverted_index.environment | 6 |
| abstract_inverted_index.frameworks. | 41 |
| abstract_inverted_index.interactive | 127 |
| abstract_inverted_index.higher-order | 115 |
| abstract_inverted_index.illustrating | 131 |
| abstract_inverted_index.limitations, | 57 |
| abstract_inverted_index.verification | 53 |
| abstract_inverted_index.applications, | 161 |
| abstract_inverted_index.corresponding | 93 |
| abstract_inverted_index.Traditionally, | 29 |
| abstract_inverted_index.time-consuming | 73 |
| abstract_inverted_index.incompleteness. | 51 |
| abstract_inverted_index.debugging/testing | 40 |
| abstract_inverted_index.higher-order-logic | 80, 91 |
| cited_by_percentile_year.max | 96 |
| cited_by_percentile_year.min | 91 |
| countries_distinct_count | 2 |
| institutions_distinct_count | 5 |
| citation_normalized_percentile.value | 0.71512436 |
| citation_normalized_percentile.is_in_top_1_percent | False |
| citation_normalized_percentile.is_in_top_10_percent | False |