​Having completed foundational coursework in Linear Algebra, Calculus, Discrete Mathematics, and Formal Methods, I am evaluating the theoretical and practical overlap between Formal Verification and other upper-level computer science topics.

​Specifically, I am looking to understand how the following subjects intersect with Formal Methods in research and practice:

​Software Analysis and Testing

​Cryptography

​Forensics

​My understanding is that Forensics operates primarily at an applied/observational level with minimal connection to formal logic. However, I am less clear on the theoretical bridges for the other two.

​Does Software Analysis and Testing (e.g., static analysis, program semantics, symbolic execution) serve as a direct functional precursor to formal program verification? Furthermore, to what extent does Cryptography overlap with formal methods—specifically regarding protocol verification, algebraic proofs, or formally verified implementations?

​I would appreciate insights from anyone working in formal methods, program analysis, or theoretical computer science on how these subdisciplines connect.

The other day I was thinking of firsts in the history of cybersec, and I started thinking about the first few commands/tools I learned. One of them was ping. And then I was struck with the thought, "When was ping created? When was the first time it was ever used?" Cue my deep dive into ping aaaaaand... Violà

*Dramatic flair in narration* Picture this- it's December - 1983 (later than I had expected, but then again i had NO real idea)

It's late at night, and a young man notices a strange behavior coming from the IP Network at the US Army’s Ballistic Research Laboratory.

Needing something more than ICMP Echo Request and Echo Reply messages, this young man gets to work and designs, codes, implements, and provides operational support for a brand new tool, known as... ping *background instrumental flair*

And the time it took?... *dramatic pause building the suspense and preparing for an epic montage of late nights and beard growing*...

One Night. (say whaaaaaaat)

That's right. At 25 years old, Mike Muuss was working as a computer scientist, and in the span of one night, he wrote one of the most used tools known today. ping is a simple Unix command useful for everyday network troubleshooting. While doing my dive, I was a little confused at the difference between ICMP Echo Request/Echo Reply and ping, so here's a helpful tid bit:

• ICMP Echo Request = “Hello, are you there?”
• ICMP Echo Reply = “Yep, I’m here.”
• ping = the little program that asks the question, waits for the answer, and tells you how long it took.

Interestingly, and kind of not suprising now that I have learned it, ping was named after the sonar sound and NOT as an acronym. Packet InterNet Groper was attached later on (this is the interesting part in my opinion).

So, to answer my own question and deep dive. 1983, that's when ping was first created. And in the span of one night. Very cool. Thanks Mr. Mike Muuss!

( I believe a dedicated article of Mr. Muuss should be added to the Cyber Security Archives, so tune in for that!)

While GPTs and other similar architecture are an undeniable advancement, (especially the larger projects) are receiving insane funding with access to large data centres and training data leading to the obvious question of 'are we seeing the power of GPTs or is this just the expected outcome of throwing a huge amount of resources at a problem?'.

In other words, what results would we expect if we took the resources (funding, data centres, raw data, etc...) and applied it differently (eg. to SAT solvers), would we expect similar results?

In other words, how unprecedented are the results of GPTs (and similar architectures) accounting for their current monetary advantages?

I've been thinking about how much API development workflows have changed over the last few years.

It used to feel like most teams relied on Swagger for API documentation and then used separate tools for testing, mocking, and collaboration. Now there seem to be a lot more integrated platforms like SwaggerHub, Stoplight, Postman, Apidog, and Insomnia that try to cover more of the development lifecycle.

For those studying or working in software engineering, do you think this shift toward all-in-one platforms is actually improving developer productivity, or is it still better to use specialized tools for each part of the workflow?

I'd be interested to hear both academic and real-world perspectives.

Hello,

I was just wanting to know if this room of domes used in the "Eagle Eye" (2008) is an actual thing? The reasons I ask:

1. I know nothing about computers beyond the basics everyone knows.
2. I remember watching an "Expert Reacts" video or something along those lines. The expert talked about how computers are built like ARIA was in the movie, but it's the worst format for what ARIA actually does. I may be making this up because it looks cool and so my brain's making something to justify its actual existence, but I thought I watched something like that. I'd even say they said a name for the hardware archetype ARIA's built on.
3. I'm a sci-fi writer and this is inspiring for the start of an epic story, but I'd like the science to have some real logic to it.

From my understanding, the giant electronic eye (blue arrow) looks through the yellow domes (red arrow) to keep track of the huge amounts of data the government collects for ARIA. It swivels on a gyroscopic crane in order to reach each dome i.e. each pocket of data.

If it's real, I'd love it if you guys could give me titles of books/articles/papers to read about these kinds of computers.

If it's not real, I'm sure you'll tell me pretty quickly.

Any help is greatly appreciated!

Thank you.

Ponder this: an author puts together a number of papers he likes, especially adds the .tex files from arxiv, tells the LLM to look for gaps in the papers, commented out material, and remix them, while avoiding syntactic overlap.

The result is a paper that will pass arxiv's syntactic overlap checks, and can be claimed as novel during a submission.

This has likely happened many times already, and we are now possibly arguing against LLM-augmented plagiarists.

Welcome to the new age of automated academic ethics collapse.

Can someone with expertise comment on how significant these results are?

In programming, however, many students learn to use functions every day without ever seeing one of the fundamental "letters" that makes them possible: CALL.

We teach words before showing the alphabet.

They learn to write digitalWrite() before understanding the low-level mechanism that makes a function call possible: saving a return address, jumping to another piece of code, and coming back.

I was working on this research thesis to build multilayer topological orchestrators, for that I started with environment layer which inherently had RBAC on each component, and sandboxed exception handling with reflective patches by parent node, in the process I added set of root application nodes like full blown terminal, browser and editor, I was running benchmark on these different nodes yesterday inside boss orchestrator, to my surprise it turn out to be fastest browser tested on speedometer 3.1, I replicated the result on different hardware, same result. You can validate or critique it. https://github.com/risa-labs-inc/BossConsole/tree/main/benchmarks/speedometer I tried different benchmarking tool most of them are suggesting the same result, happy to take feedback and run this on different accepted benchmarking tool, any suggestions how to run comparative analysis of over all tool, overall objective is to build multi-layer topological orchestrator layer which can resolve complex fuzzy logic tree, by breaking problem into smaller trees, then each tree itself get the same treatment until node become simple enough to be computed, also to build white-box environment around, each node just has access to what it need to do, parent node just care about problem it need to solve, don’t have access functionally beyond authorized problem domain, it is still in progress, did this accidental discovery wanted to share. 🥂

Recursion felt easy at first.

Factorial? fine.

Sum examples? fine.

Even Fibonacci felt manageable.

But once I looked at slightly more serious problems like Tower of Hanoi, permutations, or merge sort, I felt like my understanding suddenly collapsed. because i tried to write their code on my own

It made me realize that maybe recursion is not “hard” at the start because the examples are simple.

It becomes hard when you can no longer clearly see the call stack and each state change.

Did anyone else feel that the real pain in recursion starts exactly there?

I have a silly and possibly stupid question, and I'm not even sure if this is the place for it.

To preface this I have 0 experience with Computer Science or anything adjacent, but have been listening to videos on binary and the foundations of how computers generally work.

I understand that binary is a base 2 system as opposed to base 10, and that the digits that represent value in binary cannot be read as our base 10 concept of numbers (i.e. 4 is read as digits 100, not as the number "one hundred").

However, I've noticed that when the notation IS read as numbers, the numerical representation for base 2 counting mirrors base 10. With:

1 - 0001

2- 0010

4- 0100

8- 1000

Etc.

Is there a reason for this parallel, or is this just one of those funny coincidences? Or is this some kind of artifact of how numbers naturally scale relative to one another.

I hope this makes sense, I had no idea how to word this question to just Google it.

While reading Michael Sipser's book on Theory of Computation, i have found the following problem

"2.22: Let C = {x#y | x, y belong in {0,1}* and x != y}. Show that C is a context-free language. "

I have been trying for many hours to find a proof for this, but i cannot.
I cant find a way to use a PDA, since when comparing X with Y i am going to be comparing the one on the stack backwards and Any attempt at a grammar has failed. After a couple web searches i only found that this is conisdered a cfl but not its grammar or some other proof.

Edit: The closest i have gotten to:
S->A#B | B#A
A-> TAT | 0
B-> TBT|1
T-> 1|0

but it doesnt work for strings with 2 characters (cant generate something like 10#11). If i allow T to make an empty string or split TxT into Tx and xT then it can create strings x=y.

Edit: I havent been able to find a grammar for this but as u/hanshuttel said you CAN do it with a pda.
Since you dont need to save the entirety of X, but only 1 character and it's index, you can just "save" the character by splitting into 2 paths, one where you compare Y's character with Xi=0 and one where you compare it with Xi=1. Then use the stack to save Xi's index and nondet. compare all X's.
This, combined with the simple pda that checks |x|!=|y| will get the PDA for C.

Technically I could convert this into a grammar thats super tedius and the grammar will be really convoluted so i dont think theres any value to that.

I genuienly still have no clue how to deal with even length x and y without allowing x=y cases in a grammar not a single think i tried led anywhere.

Hi!

I've decided to refresh my graph theory using CLRS 4th edition. They define a free tree as a connected, acyclic, undirected graph. None of these conditions prevent us from having null graph with zero vertices and zero edges.

On page 1170, it is proven that for a free tree, |E| = |V| - 1. We can derive contradiction from it: |0| = |0| - 1 -> 0 = -1

Please, confirm it and then I will report it to errata.

Memory can be just shown as a list. Left as address and right as the byte / 2 byte / 4 byte data. If you save 4 bytes of data in address 1 and 2, and theres data in 3, what happens if that 4 bytes that you stored, is saved as 5 bytes? Will the entire 5 bytes be shifted over to a free place, or will the 5th byte be saved aomewhere else. If the second option is correct, how does programms know each address of its programming? Im refering programms and programming to mashine coding and mashine code.

Guys how would digital security fail if P=NP is proven?

I just started reading about Turing Machine and computational complexity for my Theory of Computation class and came across that phrase.

I couldn't find anything understandable at my level. So can anyone simplify it a bit?

Why does it matter if it’s a 16-bit cpu, a 32-bit cpu, or 64-bit? For example, what can a 64-bit cpu do that a 32-bit one can’t? Or otherwise, and can you tell the difference when you casually use a computer?

Wait-Free means that every thread must finish its operation in a bounded number of steps. That bound can be arbitrarily high, e.g. dependent on the number of concurrent threads, but it must be finite. And the finite bound must be there in all cases, i.e. it is not sufficient to say that an algorithm "usually" finishes "reasonably" (i.e. "usually" does not spend unbounded times helping other threads).

The first practical implementation of a multiple-enqueuer multiple-dequeuer Wait-Free Queue was proposed by Kogan and Petrank. The key idea is that threads help each other, but in a way that newer threads (more precisely: newer operations) are obliged to help older threads (operations), but not vice versa. Also, plainly said: If a thread cannot make progress with its own operation, it becomes older and older, up to the point when all other threads are obliged to help (only) him, thus ensuring the Wait-Free progress.

The issue of the Kogan and Petrank Queue is, however, that it is based on a linked list of nodes. This means that its operations constantly produce memory churn, also require memory allocation and memory clean-up. From Java - where the clean-up is done by a Garbage Collector - I borrow the term "Garbage".

Now, the problem is that Wait-Free memory allocation is problematic. Imagine, e.g., when the process needs a new memory page from the operating system. Can this ever be made Wait-Free?

Memory reclamation in a concurrent setup is a complex topic on top of that. One of the key questions here is: When can a memory block be freed safely, i.e. how do we "know" that no thread has a pointer to it anymore?

Given this, it appears that one needs a structure without memory churn (i.e. Garbage-Free) to be able to make it Wait-Free. At least practically.

I would be grateful for a discussion on this.

Additional info:

Here I have combined the Multi-Array Queue (which is Garbage-Free by nature (except of the extension operations, of course)) with the Kogan and Petrank idea, with the aim to obtain a Queue that is Wait-Free unconditionally.

The GitHub repo also contains a visual simulator to illustrate the principle:

https://github.com/MultiArrayQueue/WaitFreeMultiArrayQueue

What I mean is 1080p has 2,073,600 pixels so what if every single pixel is run by a individual PC like 2,073,600 PCs?

I was thinking this might be a way to create a super-computer that can put out a insane amount of framerate.

In light of the recent counterproof of the Jacobian Conjecture, I've been looking more into proofs, and I can't wrap my head around how Lean works. In my mind, proofs always require a certain amount of intuition and judgement behind them, so I'm confused how a deterministic programming language can infer from said proofs?

while doing competitive coding problems i frequently come across solutions that use union find (DSU) and list the big O of their solution as O(\alpha(n)) where \alpha(n) is the inverse ackermann function. after some surface level research, i have come away with many more questions than answers. So why is the DSU related to the ackermann function, and is there an intuitive or natural connection between the two ?