Saturday, July 26, 2025
LBNN
  • Business
  • Markets
  • Politics
  • Crypto
  • Finance
  • Energy
  • Technology
  • Taxes
  • Creator Economy
  • Wealth Management
  • Documentaries
No Result
View All Result
LBNN

New tool automates the formal verification of systems software

Simon Osuji by Simon Osuji
October 30, 2023
in Artificial Intelligence
0
New tool automates the formal verification of systems software
0
SHARES
0
VIEWS
Share on FacebookShare on Twitter


New tool automates the formal verification of systems software
Tang Family Assistant Professor of Computer Science Rongui Gu (left) and Professor of Computer Science Jason Nieh (right). Credit: Columbia Engineering

Formal systems verification, which mathematically proves that code is secure in all circumstances, is a relatively new technology. Software is getting more complex and harder to get right using traditional software testing techniques. Making software correct, safe, and secure is becoming even more critical as the use of generative AI techniques like ChatGPT to automatically write programs increases. In fact, there will be even more need for verification to ensure those automatically generated programs are correct.

Related posts

Join Our Next Livestream: Inside Katie Drummond’s Viral Interview With Bryan Johnson

Join Our Next Livestream: Inside Katie Drummond’s Viral Interview With Bryan Johnson

July 25, 2025
Samsung Galaxy Watch8 and Watch8 Classic Review: The Squircle

Samsung Galaxy Watch8 and Watch8 Classic Review: The Squircle

July 25, 2025

Recent work directed by professors Ronghui Gu and Jason Nieh introduced a new tool, Spoq, that significantly reduces the complex efforts people must use to verify real-world software and makes it possible to verify existing C systems code without modifications.

Formal verification offers a systematic and rigorous approach to software and hardware verification, helping to ensure that systems behave correctly and meet their intended specifications. With Spoq, many aspects of formal verification can be automated, significantly reducing manual proof efforts for verification. The paper was presented at the 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI) Conference on July 12, 2023.

System software forms the software foundations of our computing infrastructure. Modern system software is large, complex, and imperfect, with vulnerabilities that can be exploited to compromise the security of a system. Formal verification offers a potential solution to this problem by mathematically proving that system software can provide critical security guarantees. Unfortunately, it remains too difficult and requires too much human effort to apply in practice.

Previous tools developed by Nieh’s and Gu’s teams introduced verification techniques to make certain proofs possible that could not have been done before. Spoq’s key feature is that it automates the tedious and time-consuming parts of many proofs. “Spoq can generate results in about an hour compared to doing it manually, which can take months or years to formally verify a system,” says Xupeng Li, the paper’s lead author and a Ph.D. student with both Nieh and Gu.

Over the next few months, the lab is focused on making Spoq open-source so that formal verification can be widely deployed to secure the foundations of our computing infrastructure’s software.

The study is titled “Spoq: Scaling Machine-Checkable Systems Verification in Coq.”

More information:
Study: www.usenix.org/conference/osdi … esentation/li-xupeng

Provided by
Columbia University School of Engineering and Applied Science

Citation:
New tool automates the formal verification of systems software (2023, October 30)
retrieved 30 October 2023
from https://techxplore.com/news/2023-10-tool-automates-formal-verification-software.html

This document is subject to copyright. Apart from any fair dealing for the purpose of private study or research, no
part may be reproduced without the written permission. The content is provided for information purposes only.





Source link

Previous Post

African Court on Human and Peoples’ Rights (ACHPR) Press Release on the Situation in the Gaza Strip

Next Post

Max Q: ABL Space nears next launch

Next Post
Max Q: ABL Space nears next launch

Max Q: ABL Space nears next launch

Leave a Reply Cancel reply

Your email address will not be published. Required fields are marked *

RECOMMENDED NEWS

MBZUAI working to turn AI-driven ideas into real-world startups

MBZUAI working to turn AI-driven ideas into real-world startups

10 months ago
Safaricom Hosts Safire Connect Forum in Eldoret

Safaricom Hosts Safire Connect Forum in Eldoret

1 week ago
Tanzania penalizes a local media house for allegedly disrupting ‘national harmony’

Tanzania penalizes a local media house for allegedly disrupting ‘national harmony’

10 months ago
Helix Secures Deepwater Well Intervention Contract in West Africa

Helix Secures Deepwater Well Intervention Contract in West Africa

1 year ago

POPULAR NEWS

  • Ghana to build three oil refineries, five petrochemical plants in energy sector overhaul

    Ghana to build three oil refineries, five petrochemical plants in energy sector overhaul

    0 shares
    Share 0 Tweet 0
  • When Will SHIB Reach $1? Here’s What ChatGPT Says

    0 shares
    Share 0 Tweet 0
  • The world’s top 10 most valuable car brands in 2025

    0 shares
    Share 0 Tweet 0
  • Top 10 African countries with the highest GDP per capita in 2025

    0 shares
    Share 0 Tweet 0
  • Global ranking of Top 5 smartphone brands in Q3, 2024

    0 shares
    Share 0 Tweet 0
  • Privacy Policy
  • Contact

© 2023 LBNN - All rights reserved.

No Result
View All Result
  • Home
  • Business
  • Politics
  • Markets
  • Crypto
  • Economics
    • Manufacturing
    • Real Estate
    • Infrastructure
  • Finance
  • Energy
  • Creator Economy
  • Wealth Management
  • Taxes
  • Telecoms
  • Military & Defense
  • Careers
  • Technology
  • Artificial Intelligence
  • Investigative journalism
  • Art & Culture
  • Documentaries
  • Quizzes
    • Enneagram quiz
  • Newsletters
    • LBNN Newsletter
    • Divergent Capitalist

© 2023 LBNN - All rights reserved.